diff options
| -rw-r--r-- | lib/compat.ml4 | 10 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 18 |
2 files changed, 19 insertions, 9 deletions
diff --git a/lib/compat.ml4 b/lib/compat.ml4 index f2994edc6..67d2820a7 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -227,3 +227,13 @@ let expl_anti loc e = <:expr< $anti:e$ >> ELSE let expl_anti _loc e = e (* FIXME: understand someday if we can do better *) END + +(** Compatibility with Camlp5 6.x *) + +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 034c46e58..a77fb7cd7 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -663,16 +663,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = | ETConstrList (typ',[]) -> Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) | ETConstrList (typ',tkl) -> - Slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) + slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) + (make_sep_rules tkl) | ETBinderList (false,[]) -> Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) | ETBinderList (false,tkl) -> - Slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) + 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 @@ -686,16 +686,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = let rec symbol_of_prod_entry_key = function | Alist1 s -> Slist1 (symbol_of_prod_entry_key s) | Alist1sep (s,sep) -> - Slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string sep) | Alist0 s -> Slist0 (symbol_of_prod_entry_key s) | Alist0sep (s,sep) -> - Slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) + slist0sep (symbol_of_prod_entry_key s) (gram_token_of_string sep) | Aopt s -> Sopt (symbol_of_prod_entry_key s) | Amodifiers s -> Gram.srules' [([], Gram.action (fun _loc -> [])); ([gram_token_of_string "("; - Slist1sep ((symbol_of_prod_entry_key s), gram_token_of_string ","); + slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ","); gram_token_of_string ")"], Gram.action (fun _ l _ _loc -> l))] | Aself -> Sself |