Ssreflect Users Discussion List

[Andrej Bauer <>]

Hello,

I am trying to compile ssreflect under MacOS 10.6.8 (Intel).

The precompiled Coq 8.3pl2 which can be downloaded as a MacOS .dmg
installation bundle can't handle dynamic linking, at least not on my
PowerBookPro. I suspect it was compiled in 32-bit mode or some such.
You could want people about this issue in the documentation.

Now I have:

~/compile/ssreflect/ssreflect-1.3pl2$ ocaml -version
The Objective Caml toplevel, version 3.12.1

~/compile/ssreflect/ssreflect-1.3pl2$ coqc -v
The Coq Proof Assistant, version 8.3pl4 (April 2012)
compiled on Apr 14 2012 18:48:37 with OCaml 3.12.1

The creation of dynamic libraries goes through, but then the
compilation gets stuck like this:

coqc  -q  -R theories Ssreflect -R src Ssreflect   theories/fintype
File "/Users/andrej/compile/ssreflect/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

Might it be the case that 8.3pl4 is incompatible with ssreflect 1.3?

I would appreciate any hints.

With kind regards,

Andrej