coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Error in Ssreflect compilation

From: Michael Ganem <michael.ganem AT gmail.com>
To: coq-club AT inria.fr, Stéphane Glondu <steph AT glondu.net>
Subject: [Coq-Club] Error in Ssreflect compilation
Date: Mon, 13 Jan 2014 23:28:01 +0200

Hi,

I'm trying to compile the ssreflect package but I got the following error:

/usr/local/bin/coqc -q -I src -R theories Ssreflect theories/ssrmatching
File "/ssreflect/theories/ssrmatching.v", line 3, characters 0-30:
Error: Cannot link ml-object ssreflect.cmo to Coq code.
make[1]: *** [theories/ssrmatching.vo] Error 1
make[1]: Leaving directory `/ssreflect'
make: *** [all] Error 2

Coq is compiled in my Ubunutu system in byte mode.

Thanks,
Michael

[Coq-Club] Error in Ssreflect compilation, Michael Ganem, 01/13/2014