Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Jan 28, 2016 at 08:41:35PM +0000, Ilya Sergey wrote:
> Hi Enrico.
> 
> For some reasons, I have problems with compiling this version following the
> instructions from the INSTALL file. After running make -j2, I get the
> following:
> 
> ocamlc.opt -c -rectypes -thread  -I "." ...
> ....
> File "ssrmatching.ml4", line 166, characters 38-53:
> Error: This expression has type Term.types = Constr.t
>        but an expression was expected of type 'a * 'b
> make[1]: *** [ssrmatching.cmo] Error 2
> make: *** [all] Error 2
> 
> I use OCaml and camlp4 version 4.02.3.
> 
> Any ideas what's wrong with my setup?

Which version of Coq are you building against? (it should be visible
in the "-I ..." part you erased.

Could you please send me a full log?

Best,
-- 
Enrico Tassi