Stream: Coq devs & plugin devs

Topic: inconsistent assumptions

view this post on Zulip Jason Gross (Aug 23 2023 at 04:14):

Can someone explain this error message to me?

File "./src/Float/Primitive_ops.v", line 17, characters 0-21:
Error:
Compiled library Interval.Real.Xreal (in file /home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/mathcomp/ssreflect/eqtype.vo) makes inconsistent assumptions over library mathcomp.ssreflect.eqtype

(Is there a way I can ask votour what library lives in that .vo file?)

view this post on Zulip Jason Gross (Aug 23 2023 at 04:15):

I also see

File "./src/Poly/Datatypes.v", line 28, characters 0-22:
Error:
Compiled library Interval.Missing.Stdlib (in file /home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/mathcomp/ssreflect/eqtype.vo) makes inconsistent assumptions over library mathcomp.ssreflect.eqtype

view this post on Zulip Jason Gross (Aug 23 2023 at 04:23):

Reported at https://github.com/coq/coq/issues/17973

Last updated: Nov 29 2023 at 22:01 UTC