Ssreflect Users Discussion List

[Cyril Cohen <>]

Dear Andrej Bauer,

Yes, there is a small incompatibility between Coq >= 8.3pl3 and ssreflect 
1.3pl2.
This problem has already been mentioned on this mailing list [1], so the best
thing to do may be to point you to its archives.
I think the smallest and easiest patch to apply is the one given in Enrico's
answer [2].
(If it doesn't work, you could try one of the other solutions provided in [3])

Best regards,
-- 
Cyril Cohen

[1]
https://sympa.msr-inria.inria.fr/sympa/wwsympa-wrapper.fcgi/arc/ssreflect/2012-03/msg00000.html
[2]
https://sympa.msr-inria.inria.fr/sympa/wwsympa-wrapper.fcgi/arc/ssreflect/2012-03/msg00001.html
[3]
https://sympa.msr-inria.inria.fr/sympa/wwsympa-wrapper.fcgi/arc/ssreflect/2012-03/msg00002.html