Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Reynald,

  you probably made no mistake: compilation of the trunk version of ssreflect
has been broken for 23 days now, as you can check on the online interface of 
the
daily bench run:

http://ssr.msr-inria.inria.fr/hudson/

You can also access the last log (tonight compilation):

http://ssr.msr-inria.inria.fr/hudson/job/coqfinitegroup---coq_trunk---ssreflect1.3_trunk/1031/console

This long delay is mainly due to the fact that most of us (both in the 
MathComp
group and Coq developers) have been on holidays or away from their office for
the three last weeks.

From next week on, there should be more manpower back so that we start fixing
this. Sorry about that.

By the way, which kind of features in the trunk version of Coq would you like 
to
combine with ssreflect?

Sorry again for these inconvenience.

Best,

assia

Le 10/08/2011 14:23, Reynald Affeldt a écrit :
> 
> 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
> 
>