passage a ocaml 3.06

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 8 insertions, 7 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index d665ad5759..731bb5e646 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -144,7 +144,7 @@ let extend_grammar gram =
 (* Add a grammar rules for tactics *)
 type grammar_tactic_production =
   | TacTerm of string
-  | TacNonTerm of loc * (Gramext.g_symbol * argument_type) * string option
+  | TacNonTerm of loc * (Gram.te Gramext.g_symbol * argument_type) * string option
 
 let make_prod_item = function
   | TacTerm s -> (Gramext.Stoken (Extend.terminal s), None)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 9f9e348463..73f9e424e3 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -31,7 +31,7 @@ val extend_grammar : all_grammar_command -> unit
 (* Add grammar rules for tactics *)
 type grammar_tactic_production =
   | TacTerm of string
-  | TacNonTerm of loc * (Gramext.g_symbol * Genarg.argument_type) * string option
+  | TacNonTerm of loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
   string -> (string * grammar_tactic_production list) list -> unit
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2d444fcbbe..ddea9997dd 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -108,7 +108,7 @@ type ext_kind =
   | ByGrammar of
       typed_entry * Gramext.position option *
       (string option * Gramext.g_assoc option *
-       (Gramext.g_symbol list * Gramext.g_action) list) list
+       (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
   | ByGEXTEND of (unit -> unit) * (unit -> unit)
 
 let camlp4_state = ref []
@@ -117,6 +117,7 @@ let camlp4_state = ref []
    extensions. *)
 module Gram =
   struct
+    type te = Token.t
     type parsable = G.parsable
     let parsable = G.parsable
     let tokens = G.tokens
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 628f4035e9..9acf97078e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Vernacexpr
 
 val lexer : Token.lexer
 
-module Gram : Grammar.S
+module Gram : Grammar.S with type te = Token.t
 
 type grammar_object
 type typed_entry
@@ -30,7 +30,7 @@ val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
 val grammar_extend :
   typed_entry -> Gramext.position option ->
     (string option * Gramext.g_assoc option *
-     (Gramext.g_symbol list * Gramext.g_action) list) list
+     (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
 
 val remove_grammars : int -> unit
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index fbee5ff274..76430e1c45 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -132,7 +132,7 @@ let pr_red_expr (pr_constr,pr_ref) = function
   | Pattern l ->
       hov 1 (str "Pattern" ++ 
         prlist(fun (nl,c) -> prlist (pr_arg int) nl ++ (pr_arg pr_constr) c) l)
-  | (Red true | Cbv _ | Lazy _) -> error "Shouldn't be accessible from user"
+  | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr (s,c) ->
       hov 1 (str s ++ pr_arg pr_constr c)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9c65bdbbfe..4f8c81c704 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -266,7 +266,7 @@ open Vernacexpr
 (*               declaration of the AUTOHINT library object               *)
 (**************************************************************************)
 
-let eager o = ref (Lazy.Value o)
+let eager = Lazy.lazy_from_val
 
 (* If the database does not exist, it is created *)
 (* TODO: should a warning be printed in this case ?? *)