Source: coqeal Version: 1.1.1-3 Severity: serious Tags: ftbfs trixie sid https://buildd.debian.org/status/logs.php?pkg=coqeal&ver=1.1.1-3%2Bb2
... COQC refinements/bareiss_eff.v File "./refinements/seqmx_complements.v", line 46, characters 0-58: Warning: The default value for Typeclasses Opaque and Typeclasses Transparent locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding typeclass transparency hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Typeclasses Transparent foo.". This is supported since Coq 8.15. [deprecated-typeclasses-transparency-without-locality,deprecated] COQC refinements/multipoly.v File "./refinements/multipoly.v", line 13, characters 0-48: Error: Cannot find a physical path bound to logical path mpoly with prefix SsrMultinomials. make[3]: *** [Makefile.coq:844: refinements/multipoly.vo] Error 1