summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/pcoq.ml425
-rw-r--r--parsing/pcoq.mli4
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