Your message dated Wed, 26 Aug 2026 15:35:58 +0000
with message-id <[email protected]>
and subject line Bug#1145675: fixed in rocq-micromega-plugin 1.1.1-2
has caused the Debian Bug report #1145675,
regarding libcoq-micromega-plugin: Missing ocaml/coq dependencies
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact [email protected]
immediately.)
--
1145675: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1145675
Debian Bug Tracking System
Contact [email protected] with problems
--- Begin Message ---
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
--- End Message ---
--- Begin Message ---
Source: rocq-micromega-plugin
Source-Version: 1.1.1-2
Done: Stéphane Glondu <[email protected]>
We believe that the bug you reported is fixed in the latest version of
rocq-micromega-plugin, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to [email protected],
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Stéphane Glondu <[email protected]> (supplier of updated rocq-micromega-plugin
package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing [email protected])
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Wed, 26 Aug 2026 17:20:15 +0200
Source: rocq-micromega-plugin
Architecture: source
Version: 1.1.1-2
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <[email protected]>
Changed-By: Stéphane Glondu <[email protected]>
Closes: 1145675
Changes:
rocq-micromega-plugin (1.1.1-2) unstable; urgency=medium
.
* Team upload
* Add missing ocaml/coq dependencies (Closes: #1145675)
Checksums-Sha1:
9feb72d037777700408f92fba6ba2b75f8ad4cab 2460 rocq-micromega-plugin_1.1.1-2.dsc
a7575d88e8afe76a9535b4c805fe4736919b208a 2552
rocq-micromega-plugin_1.1.1-2.debian.tar.xz
e93051f0c3456d6b88c67eb474314f8a6529e38e 265392
rocq-micromega-plugin_1.1.1-2.git.tar.xz
a2a598fef98b49f1e4ea06fb8f9f9ab5d793799a 17716
rocq-micromega-plugin_1.1.1-2_source.buildinfo
Checksums-Sha256:
3e2d21b8a78de496d22b10f525e11c426a72f601a5dbd2d178f490e3bbe503c5 2460
rocq-micromega-plugin_1.1.1-2.dsc
760f32129d7f971286008c7fb4d3406a9d9a646ad6524e010396dc95014005ed 2552
rocq-micromega-plugin_1.1.1-2.debian.tar.xz
9f389d53cb0e0e6f8ec6cf777f1651b3220adffabaff09010923f01cec15400d 265392
rocq-micromega-plugin_1.1.1-2.git.tar.xz
15cf4bcd48c9687e87c4d30188e7772ed4f0ca88182ba322dc8c3263e57bce1b 17716
rocq-micromega-plugin_1.1.1-2_source.buildinfo
Files:
edf1481606a87bffb1eb5916e3dad4ef 2460 math optional
rocq-micromega-plugin_1.1.1-2.dsc
ad104d3884c980546f1d0e9816190198 2552 math optional
rocq-micromega-plugin_1.1.1-2.debian.tar.xz
f6ac29ad92611d62c75875406fad5b3f 265392 math optional
rocq-micromega-plugin_1.1.1-2.git.tar.xz
3ab807b4d332f8e707119780cd6474e1 17716 math optional
rocq-micromega-plugin_1.1.1-2_source.buildinfo
Git-Tag-Info: tag=57be73a25488c121398be1dc6cb2374c81dc4b8d
fp=6de24e97eca886cc56e6250e21b8eef1b1893081
Git-Tag-Tagger: Stéphane Glondu <[email protected]>
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCgAdFiEEN02M5NuW6cvUwJcqYG0ITkaDwHkFAmqPBOUACgkQYG0ITkaD
wHm7IRAA6e5qY6VCSSybR7CcaHKKr+ogZ5YmzJYUCAMBNv4EFvJdMGQ6n0Lc+KPy
cqUulKZJzFu+KcjxIvxjOhtuFTaNUlitVd2L5oWXhz/YqOCWGefWhYbayh2+570/
eAVgwRFHUIPmXbhASu5brAChxebssHgqQvs24YswMadOGvn1CsxFHqj36cNWdE2C
btVEoRZfSRYcqsFZdm4/JvmAzeiW27WSEvq06U8tt1tx9XNvEQe1IVRZe/VZqoJ/
Lak+xVHWm7Jbpw16+HmjANDi3NnCsZFE5oqjhHuGKG6aMnnOuO+Lj4/Sty42tUiq
q7MkgHGBZneHTY8Q1q2+c3wdldxsTFj0g2wbi44J4S9q67Yr+whNJgOPBMGumtU4
fCv0VCXck5rXiJhXsyubbRlZN+hIPnpBb4DX9E4JsmYfzl7QCjvTdXvb7ZWoa/vF
wAvL6nU3evvp8FSyyJ/LXp5lzOHCheT8csVM5O5cld4Wy5WAFlm+xS14otykcNUB
Y9nj2IMzLoANV+iF5mPwWrfw2eEIgtrOaiw2nyQ6vOnzNAfKwNTr7M4OHxDIWeG/
hyiyYBP1MwqeiNe8Bj2kghY97WuqkJhegffeXJWSEq0E/HTO2s4AqnOoWI7Odd89
PD6uiH/8O+R8jLM7RXPTcWrTW6F9vcCPvjmbShQ5paIS6ELY9Pk=
=07Hz
-----END PGP SIGNATURE-----
pgpYyKwlh3u46.pgp
Description: PGP signature
--- End Message ---
