The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

2015-01-25 8:32 GMT-03:00 Enrico Tassi <enrico.tassi AT inria.fr>:

On Sat, Jan 24, 2015 at 09:25:57PM -0300, Leonardo Rodriguez wrote:
> Hi Club,
>
> I'm trying to install Ssreflect 1.5 in Coq 8.5pl5 (development version). I
> have

Where did you get ssreflect?  Is it the official tarball from
http://ssr.msr-inria.inria.fr ?

Exactly, I got it from there.

I guess you mean Coq 8.4pl5

Yes :)

> installed Ocaml 3.12.1 and Camlp5 6.06.
>
> I got an error message after doing "make" in the ssreflect folder.
>
> File "src/ssrmatching.mli", line 76, characters 14-34:
> Error: Unbound type constructor glob_constr_and_expr
> make[1]: *** [src/ssrmatching.cmi] Error 2

Have you properly set COQBIN?

That seems to be OK. I googled the error, the error message is very similar to the following:
 

http://coq-bench.github.io/Linux-x86_64-4.01.0-1.2.0/stable/hott/ssreflect/1.5.0/2014-12-05_16-18-29.html
 

Best,
--

Thanks.

 

Enrico Tassi