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

5 files changed, 3 insertions, 19 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index a02b7babc..cc378ceda 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -11,7 +11,6 @@
 open Genarg
 open Q_util
 open Egramml
-open Pcoq
 open Compat
 
 let loc = Loc.ghost
@@ -264,7 +263,6 @@ let declare_vernac_argument loc s pr cl =
         ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") }
       >> ]
 
-open Vernacexpr
 open Pcoq
 open Pcaml
 open PcamlSig
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index f4d3c41f6..8943b2b63 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -8,16 +8,10 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
-open Glob_term
-open Term
-open Names
-open Pattern
 open Q_util
-open Pp
 open Compat
 open Pcaml
 open PcamlSig
-open Misctypes
 
 let loc = Loc.ghost
 let dloc = <:expr< Loc.ghost >>
@@ -34,9 +28,9 @@ EXTEND
       <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
   ;
   sort:
-    [ [ "Set"  -> GSet
-      | "Prop" -> GProp
-      | "Type" -> GType None ] ]
+    [ [ "Set"  -> Misctypes.GSet
+      | "Prop" -> Misctypes.GProp
+      | "Type" -> Misctypes.GType None ] ]
   ;
   ident:
     [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index aae1d9de2..3d39d13d7 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Q_util
 open Compat
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index be021467b..895584703 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -8,9 +8,7 @@
 
 (* This file defines standard combinators to build ml expressions *)
 
-open Extrawit
 open Compat
-open Pp
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -51,9 +49,6 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
-open Vernacexpr
-open Genarg
-
 let rec mlexpr_of_prod_entry_key = function
   | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3074337f6..db8c51386 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -10,9 +10,7 @@
 
 open Pp
 open Util
-open Genarg
 open Q_util
-open Q_coqast
 open Argextend
 open Tacextend
 open Pcoq