Bug#1038672: mathcomp-abel FTBFS: Error: The reference fact_smonotone was not found in the current environment.
Source: mathcomp-abel
Version: 1.2.1-1
Severity: serious
Tags: ftbfs trixie sid
https://buildd.debian.org/status/logs.php?pkg=mathcomp-abel&ver=1.2.1-1%2Bb6
...
dh_auto_build -a
make -j4 "INSTALL=install --strip-program=true"
make[1]: Entering directory '/<<PKGBUILDDIR>>'
coq_makefile -f _CoqProject -o Makefile.coq
make --no-print-directory -f Makefile.coq
COQDEP VFILES
COQC theories/xmathcomp/various.v
COQC theories/xmathcomp/char0.v
File "./theories/xmathcomp/char0.v", line 104, characters 14-21:
Warning: Notation rmorphX is deprecated since mathcomp 1.17.0.
Use rmorphXn instead. [deprecated-syntactic-definition,deprecated]
File "./theories/xmathcomp/char0.v", line 104, characters 14-21:
Warning: Notation rmorphX is deprecated since mathcomp 1.17.0.
Use rmorphXn instead. [deprecated-syntactic-definition,deprecated]
File "./theories/xmathcomp/various.v", line 1168, characters 34-48:
Error: The reference fact_smonotone was not found in the current environment.
make[3]: *** [Makefile.coq:844: theories/xmathcomp/various.vo] Error 1
Reply to: