Imported Upstream version 8.3pl1upstream/8.3pl1

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