Ssreflect Users Discussion List

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.''