Ssreflect Users Discussion List

[Jose Grimm <>]

Le 18/12/12 17:48, Enrico Tassi a écrit :
> On Tue, Dec 18, 2012 at 05:39:04PM +0100, Jose Grimm wrote:
> > I'm using coq8.4, together with the ssreflect from coqfinitgroup/trunk
> >
> > The Coq Proof Assistant, version 8.4 (September 2012)
> > compiled on Sep 18 2012 18:24:06 with OCaml 3.12.0
> This bug was fixed in revision 4155, commit title:
>
>    "patterns with (X in t) part fix"
>
> Could you double check you are really running revision 4165?
> Is seems to work fine here.
Well, strace shows me that the file ssreflect.cmxs comes from the directory
coq8-4/user-contrib/Ssreflect, and was created three months ago.

How do I recreate this file ? should I execute make in the directory
ssreflect/ssreflect1.3_v8.4, followed by make install ? Ids is the 
necessary to  recomplies all files in the trunk ?

Thanks in advance,
 José

Attachment: smime.p7s
Description: Signature cryptographique S/MIME