diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 25 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 4 |
3 files changed, 20 insertions, 13 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 304640b2..a00bb689 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: g_vernac.ml4 13699 2010-12-09 19:24:45Z herbelin $ *) open Pp @@ -233,7 +233,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 90a9220f..14d50e6c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id: pcoq.ml4 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: pcoq.ml4 13690 2010-12-06 16:15:54Z glondu $ i*) open Pp open Util @@ -145,6 +145,11 @@ module Gram = G.delete_rule e pil end +IFDEF CAMLP5_6_02_1 THEN +let entry_print x = Gram.Entry.print !Pp_control.std_ft x +ELSE +let entry_print = Gram.Entry.print +END let camlp4_verbosity silent f x = let a = !Gramext.warning_verbose in @@ -631,16 +636,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 +659,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 diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e4566e77..4eb06088 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: pcoq.mli 13690 2010-12-06 16:15:54Z glondu $ i*) open Util open Names @@ -23,6 +23,8 @@ open Libnames module Gram : Grammar.S with type te = Compat.token +val entry_print : 'a Gram.Entry.e -> unit + (**********************************************************************) (* The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using |