Ssreflect Users Discussion List

[Alain Lichnewsky <>]

Bonjour;

I run into difficulties to compile ssreflect under Linux with
the following configuration:
    - ssreflect : ssreflect-1.4-coq8.4.tar.gz
    - Coq:
         The Coq Proof Assistant, version 8.4pl2 (August 2013)
         compiled on Aug 02 2013 21:39:23 with OCaml 4.00.1
    - Caml:The OCaml compiler, version 4.00.1

Error message terminating make:

File "src/ssrmatching.ml4", line 889, characters 0-7:
Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead
File "src/ssrmatching.ml4", line 1:
Error: Preprocessor error
make[1]: *** [src/ssrmatching.cmo] Erreur 2

I have tried to simply apply the suggestions of replacing
GEXTEND by EXTEND, wich leads to another error: (see diff below)

File "src/ssrmatching.ml4", line 838, characters 53-70:
Error: This expression has type Tok.t Stream.t -> char
       but an expression was expected of type Pcoq.Gram.token_stream -> 'a
       Type Tok.t Stream.t is not compatible with type
         Pcoq.Gram.token_stream =
           (Pcoq.Gram.Token.t * Pcoq.Gram.token_info) Stream.t

Is this issue known? Does it have a solution?

Thanks
Alain


Diff (git format):
+++++++++++++++++++++++++++++++++++++++++++++
alain@alain-linux:$ git diff
diff --git a/src/ssrmatching.ml4 b/src/ssrmatching.ml4
index 1eb244d..d816a9b 100644
--- a/src/ssrmatching.ml4
+++ b/src/ssrmatching.ml4
@@ -886,7 +886,7 @@ ARGUMENT EXTEND cpattern
 | [ "Qed" constr(c) ] -> [ mk_lterm c ]
 END

-GEXTEND Gram
+EXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr ->
     let pattern = mk_term k c in
@@ -902,7 +902,7 @@ ARGUMENT EXTEND lcpattern
 | [ "Qed" lconstr(c) ] -> [ mk_lterm c ]
 END

-GEXTEND Gram
+EXTEND Gram
   GLOBAL: lcpattern;
   lcpattern: [[ k = ssrtermkind; c = lconstr ->
     let pattern = mk_term k c in
+++++++++++++++++++++++++++++++++++++++++++++