Hello, On Sun, Dec 13, 2020 at 06:28:01PM +0900, Nobuhiro Ban wrote:
> I cannot use the ssreflect library in my Debian coq env (amd64 testing). > > the code: > > Require Import mathcomp.ssreflect.ssreflect. > > gets an error: > > > Compiled library mathcomp.ssreflect.ssreflect (in file > > /usr/lib/coq/user-contrib/mathcomp/ssreflect/ssreflect.vo) makes > > inconsistent assumptions over library Coq.Init.Ltac I have now recompiled the package (and updated to a newer version), so it is at least solved for the moment. > I think this package should depend on "libcoq-ocaml-<Hash>", > because "coq-<CoqVer>+<OCamlVer>" is insufficient for binNMUs. I am not sure what exactly has to be done, will have to consult with the teamm. -Ralf.
