Ssreflect Users Discussion List

["Lucian M. Patcas" <>]

Hello,

I've tried to compile Ssreflect 1.3pl1 on Mac without success. Here are some details:

MacOS 10.6.8
Ocaml 3.12.0 binary distribution
camlp5
Coq 8.3pl2 binary distribution

The output of make is the following:

mkdir -p bin
make -f Makefile.coq all
ocamlc.opt -c -rectypes  -I src -I /usr/local/lib/coq/kernel -I /usr/local/lib/coq/lib -I /usr/local/lib/coq/library -I /usr/local/lib/coq/parsing -I /usr/local/lib/coq/pretyping -I /usr/local/lib/coq/interp -I /usr/local/lib/coq/proofs -I /usr/local/lib/coq/tactics -I /usr/local/lib/coq/toplevel -I /usr/local/lib/coq/plugins/cc -I /usr/local/lib/coq/plugins/dp -I /usr/local/lib/coq/plugins/extraction -I /usr/local/lib/coq/plugins/field -I /usr/local/lib/coq/plugins/firstorder -I /usr/local/lib/coq/plugins/fourier -I /usr/local/lib/coq/plugins/funind -I /usr/local/lib/coq/plugins/groebner -I /usr/local/lib/coq/plugins/interface -I /usr/local/lib/coq/plugins/micromega -I /usr/local/lib/coq/plugins/nsatz -I /usr/local/lib/coq/plugins/omega -I /usr/local/lib/coq/plugins/quote -I /usr/local/lib/coq/plugins/ring -I /usr/local/lib/coq/plugins/romega -I /usr/local/lib/coq/plugins/rtauto -I /usr/local/lib/coq/plugins/setoid_ring -I /usr/local/lib/coq/plugins/subtac -I /usr/local/lib/coq/plugins/subtac/test -I /usr/local/lib/coq/plugins/syntax -I /usr/local/lib/coq/plugins/xml -I /usr/local/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/local/lib/ocaml -I . -I /usr/local/lib/coq/kernel -I /usr/local/lib/coq/lib -I /usr/local/lib/coq/library -I /usr/local/lib/coq/parsing -I /usr/local/lib/coq/pretyping -I /usr/local/lib/coq/interp -I /usr/local/lib/coq/proofs -I /usr/local/lib/coq/tactics -I /usr/local/lib/coq/toplevel -I /usr/local/lib/coq/plugins/cc -I /usr/local/lib/coq/plugins/dp -I /usr/local/lib/coq/plugins/extraction -I /usr/local/lib/coq/plugins/field -I /usr/local/lib/coq/plugins/firstorder -I /usr/local/lib/coq/plugins/fourier -I /usr/local/lib/coq/plugins/funind -I /usr/local/lib/coq/plugins/groebner -I /usr/local/lib/coq/plugins/interface -I /usr/local/lib/coq/plugins/micromega -I /usr/local/lib/coq/plugins/nsatz -I /usr/local/lib/coq/plugins/omega -I /usr/local/lib/coq/plugins/quote -I /usr/local/lib/coq/plugins/ring -I /usr/local/lib/coq/plugins/romega -I /usr/local/lib/coq/plugins/rtauto -I /usr/local/lib/coq/plugins/setoid_ring -I /usr/local/lib/coq/plugins/subtac -I /usr/local/lib/coq/plugins/subtac/test -I /usr/local/lib/coq/plugins/syntax -I /usr/local/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/ssreflect.ml

Error while loading "/usr/local/lib/coq/parsing/grammar.cma": interface mismatch on Plexing.
File "src/ssreflect.ml", line 1, characters 0-1:
Error: Preprocessor error

make[1]: *** [src/ssreflect.cmo] Error 2
make: *** [all] Error 2

Any help is much appreciated.

Thank you,
Lucian