Ssreflect Users Discussion List

[Reynald Affeldt <>]

Hello,

My understanding of 
coqfinitgroup/trunk/ssreflect/00WHATSHERE 
is that:
- you should compile /coqfinitgroup/trunk/ssreflect/ssreflect1.3_trunk
- with Coq trunk
- to be able to compile the theories in /coqfinitgroup/trunk/

But this gives the following error message:
ssrcoq  -q  -dont-load-proofs -I .    -compile prime
File "/coqfinitgroup/trunk/prime.v", line 308, characters 41-42:
Syntax error: ',' or ')' expected after [constr:operconstr level 200] (in 
[constr:operconstr]).
(prime.v:308: reflect (n < 2 \/ exists2 d, 1 < d < n & d %| n) (~~ prime n).)

Could you help spot my mistake?

      Reynald