The Coq mailing list

[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 ?

I guess you mean Coq 8.4pl5

> 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?

Best,
-- 
Enrico Tassi