Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sun, Mar 11, 2012 at 07:16:31PM +0100, Nuno Gaspar wrote:
> Hello.
> 
> I'm not able to compile ssreflect on my Mac Lion. My config is the
> following:
> 
> >coqc -v
> The Coq Proof Assistant, version 8.3pl3 (December 2011)
> compiled on Dec 22 2011 12:48:25 with OCaml 3.12.1
> 
> I cannot compile the dynamic loadable plugin, but that seems to be a Lion
> issue. Anyway, for the static version I get the following error:
> 
> File ".../ssreflect-1.3pl2/theories/fintype.v", line 132, characters 44-45:
> Error: In environment
> T : eqType
> e : seq ?15
> The term "T" has type "eqType" while it is expected to have type

Coq 8.3pl3 changed the scoping rules for coercions, an we did not
release an update. Just add this line in ssreflect.v just after
Declare ML Module "ssreflect".

Global Set Automatic Coercions Import.

Cheers
-- 
Enrico Tassi