Package: libcoq-micromega-plugin Version: 1.1.1-1 Severity: serious Tags: ftbfs patch Control: affects -1 src:ssreflect
https://buildd.debian.org/status/fetch.php?pkg=ssreflect&arch=amd64&ver=2.6.0-3%2Bb1&stamp=1787752532&raw=0 ... ROCQ compile algebra/binnums.v File "./algebra/binnums.v", line 2, characters 0-51: Error: Compiled library micromega_plugin.PosDef (in file /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/micromega_plugin/PosDef.vo) makes inconsistent assumptions over library Corelib.Init.Prelude make[4]: *** [Makefile.coq:815: algebra/binnums.vo] Error 1 Fix: --- rocq-micromega-plugin-1.1.1/debian/control 2026-07-27 22:07:30.000000000 +0300 +++ rocq-micromega-plugin-1.1.1/debian/control 2026-07-27 22:07:30.000000000 +0300 @@ -21,7 +21,7 @@ Package: libcoq-micromega-plugin Architecture: any -Depends: ${misc:Depends} +Depends: ${misc:Depends}, ${ocaml:Depends}, ${coq:Depends} Recommends: coq Provides:${coq:Provides} Description: Semi-decision procedures for arithmetic in Rocq
