diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 21:11:39 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 21:11:39 +0000 |
| commit | 8d3a8edab6377823e620f7a22ccfcdcd869bb5a7 (patch) | |
| tree | 5fa0de509fab318605e9a0b285b32e4e1f6c3eec /parsing | |
| parent | e216c2de60d1d8b1fd35169257349fa4c257a516 (diff) | |
Support for camlp5 6.02.0 (Closes: #2432)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13642 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml4 | 18 |
1 files changed, 9 insertions, 9 deletions
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 |