Bug#1038675: coqeal FTBFS: Error: Cannot find a physical path bound to logical path mpoly with prefix SsrMultinomials.
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
Reply to: