From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 16 Nov 2010 20:25:56 +0000 (+0000)
Subject: Support for camlp5 6.02.0 (Closes: #2432)
X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=501c9cb6ff7c903974123284fe795cdcaab8f300

Support for camlp5 6.02.0 (Closes: #2432)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13641 85f007b7-540e-0410-9357-904b9bb8a0f7
---

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 9b6bb19..a77c2bc 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -65,3 +65,15 @@ let unloc = M.unloc
 let join_loc = M.join_loc
 type token = M.token
 type lexer = M.lexer
+
+IFDEF CAMLP5_6_00 THEN
+
+let slist0sep x y = Gramext.Slist0sep (x, y, false)
+let slist1sep x y = Gramext.Slist1sep (x, y, false)
+
+ELSE
+
+let slist0sep x y = Gramext.Slist0sep (x, y)
+let slist1sep x y = Gramext.Slist1sep (x, y)
+
+END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 4719e6d..5d37f4a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -631,16 +631,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
     | ETConstrList (typ',[]) ->
         Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
     | ETConstrList (typ',tkl) ->
-        Gramext.Slist1sep
-          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
-	   make_sep_rules tkl)
+        Compat.slist1sep
+          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+          (make_sep_rules tkl)
     | ETBinderList (false,[]) ->
         Gramext.Slist1
 	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
     | ETBinderList (false,tkl) ->
-        Gramext.Slist1sep
-	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
-	   make_sep_rules tkl)
+        Compat.slist1sep
+          (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+          (make_sep_rules tkl)
     | _ ->
     match interp_constr_prod_entry_key assoc from forpat typ with
       | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
@@ -654,16 +654,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 let rec symbol_of_prod_entry_key = function
   | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
-      Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
+      Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
   | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
   | Alist0sep (s,sep) ->
-      Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
+      Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
   | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
   | Amodifiers s ->
        Gramext.srules
         [([], Gramext.action(fun _loc -> []));
          ([Gramext.Stoken ("", "(");
-           Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ","));
+           Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
            Gramext.Stoken ("", ")")],
 	   Gramext.action (fun _ l _ _loc -> l))]
   | Aself -> Gramext.Sself