Remove some more "open" and dead code thanks to OCaml4 warnings

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

7 files changed, 5 insertions, 30 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 880d4b8ce1..ade579c69c 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -272,9 +272,9 @@ let recover_notation_grammar ntn prec =
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
-type frozen_t = all_grammar_command list * Lexer.frozen_t
+type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
 
-let freeze () = (!grammar_state, Lexer.freeze ())
+let freeze () : frozen_t = (!grammar_state, Lexer.freeze ())
 
 (* We compare the current state of the grammar and the state to unfreeze,
    by computing the longest common suffixes *)
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index 75205c9644..be584b5c8c 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Genarg
 
 (* This file defines extra argument types *)
@@ -30,7 +28,7 @@ let wit_tactic = function
   | 3 -> wit_tactic3
   | 4 -> wit_tactic4
   | 5 -> wit_tactic5
-  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
 
 let globwit_tactic = function
   | 0 -> globwit_tactic0
@@ -39,7 +37,7 @@ let globwit_tactic = function
   | 3 -> globwit_tactic3
   | 4 -> globwit_tactic4
   | 5 -> globwit_tactic5
-  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
 
 let rawwit_tactic = function
   | 0 -> rawwit_tactic0
@@ -48,7 +46,7 @@ let rawwit_tactic = function
   | 3 -> rawwit_tactic3
   | 4 -> rawwit_tactic4
   | 5 -> rawwit_tactic5
-  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+  | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
 
 let tactic_genarg_level s =
   if String.length s = 7 && String.sub s 0 6 = "tactic" then
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index bc2803ae5e..6506af0a1a 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Constrexpr
 open Tacexpr
-open Vernacexpr
 open Misctypes
 open Genredexpr
 open Tok
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 2e83f71638..a0ea5c6dea 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -13,12 +13,6 @@
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
 
 
-open Flags
-open Util
-open Names
-open Nameops
-open Reduction
-open Term
 open Libnames
 open Constrexpr
 open Constrexpr_ops
@@ -38,13 +32,8 @@ struct
   let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac"
 end
 
-open Glob_term
 open ObligationsGram
-open Util
-open Tok
 open Pcoq
-open Prim
-open Constr
 
 let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e9b91dbbf8..6d82a65043 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -18,8 +18,6 @@ open Extend
 open Vernacexpr
 open Locality
 open Decl_kinds
-open Genarg
-open Goptions
 open Declaremods
 open Misctypes
 
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 1527fa64b8..37d2b332d9 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -10,10 +10,8 @@ open Pp
 open Errors
 open Util
 open Names
-open Term
 open Pcoq
 open Glob_term
-open Genarg
 open Tacexpr
 open Libnames
 open Globnames
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 3a0840a7e1..04b5e46730 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -11,11 +11,7 @@ open Compat
 open Tok
 open Errors
 open Util
-open Names
 open Extend
-open Libnames
-open Glob_term
-open Topconstr
 open Genarg
 open Tacexpr
 open Extrawit
@@ -111,7 +107,6 @@ let weaken_entry x = Gramobj.weaken_entry x
 
 module type Gramtypes =
 sig
-  open Decl_kinds
   val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
   val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry
 end
@@ -475,7 +470,6 @@ let level_stack =
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
 (* first LeftA, then RightA and NoneA together *)
-open Ppextend
 
 let admissible_assoc = function
   | LeftA, Some (RightA | NonA) -> false