Ssreflect Users Discussion List

[bertot <>]

On 11/3/12 7:16 PM, 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

 "pred_sort ?21".

make[1]: *** [theories/fintype.vo] Error 1

make: *** [all] Error 2

I do realize that your INSTALL file says the requirements are Coq 8.3 or 8.3pl1, but the last email regarding the MAP school it indicated us to have Coq 8.3pl3 and ssreflect1.3pl2.

Should I downgrade my Coq version or should it compile with 8.3pl3 ?

Thank you.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.

I made a mistake when writing that coq-8.3pl3 was required.

Yves