Ssreflect Users Discussion List

[Christian Doczkal <>]

Hi

Thanks for the pointer. The problem affects my home machine which I cannot 
access at the moment. The gentoo ebuild appears to override the default and 
compile camlp5 in strict mode. I'll report later this evening whether this 
fixes the problem.

Regards
Christian




On 06.09.2012, at 00:24,  wrote:

> what does
> 
> camlp5 -pmode
> 
> output?
> 
> AFAIU you require camlp5 to be built in transitional mode rather than 
> strict mode <http://pauillac.inria.fr/~ddr/camlp5/doc/html/strict.html>.
> 
> On Thu, 6 Sep 2012, Christian Doczkal wrote:
> 
>> Hello
>> 
>> I have trouble building the contents of
>> 
>>      ssreflect-1.4-coq8.4.tar.gz
>> 
>> When I unpack the source and run make I get the following errors:
>> 
>> File "src/ssrmatching.ml4", line 889, characters 0-7:
>> Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead
>> Preprocessing error on file src/ssrmatching.ml4
>> 
>> ...
>> 
>> File "src/ssreflect.ml4", line 481, characters 0-7:
>> Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead
>> Preprocessing error on file src/ssreflect.ml4
>> 
>> Here are the program versions I use:
>> 
>> $ coqc --version
>> The Coq Proof Assistant, version 8.4 (September 2012)
>> compiled on Sep 05 2012 22:28:55 with OCaml 3.12.1
>> $ camlp5 -v
>> Camlp5 version 6.02.3 (ocaml 3.12.1)
>> 
>> OS: Gentoo Linux
>> 
>> Remark: I recompiled everything using camlp5 6.06 but this didn't help
>> 
>> Can someone tell me what I'm doing wrong? Any help would be appreciated.
>> 
>> Regards
>> Christian
>> 
>> 
>> 
> 
> -- 
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''