This patch removes unused "open" (automatically generated from

compiler warnings).

I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.

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

6 files changed, 0 insertions, 24 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c077fbe83..f99d8c109 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -612,7 +612,6 @@ let pr_red_flag pr r =
      pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
      hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
 
-open Genarg
 
 let pr_metaid id = str"?" ++ pr_id id
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 50baf36f8..7118388cb 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -220,7 +220,6 @@ let rec pr_glob_generic prc prlc prtac prpat x =
       try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
-open Closure
 
 let rec pr_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
@@ -543,7 +542,6 @@ let linfo = 5
 
 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
-open Closure
 
 (** A printer for tactics that polymorphically works on the three
     "raw", "glob" and "typed" levels; in practice, the environment is
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 70094b48c..748e5297b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -8,8 +8,6 @@
 
 open Pp
 open Names
-open Nameops
-open Nametab
 
 let pr_located = Loc.pr_located
 
@@ -20,14 +18,10 @@ open Extend
 open Vernacexpr
 open Ppconstr
 open Pptactic
-open Glob_term
-open Genarg
 open Libnames
-open Ppextend
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
-open Tacinterp
 open Declaremods
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d81a3389f..86b2da2eb 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -18,12 +18,7 @@ open Nameops
 open Term
 open Termops
 open Declarations
-open Inductive
-open Inductiveops
-open Sign
-open Reduction
 open Environ
-open Declare
 open Impargs
 open Libobject
 open Libnames
diff --git a/printing/printer.ml b/printing/printer.ml
index 33d099289..70a90b8ea 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -10,13 +10,9 @@ open Pp
 open Errors
 open Util
 open Names
-open Nameops
 open Term
 open Sign
 open Environ
-open Global
-open Declare
-open Libnames
 open Globnames
 open Nametab
 open Evd
@@ -24,10 +20,8 @@ open Proof_type
 open Refiner
 open Pfedit
 open Constrextern
-open Tacexpr
 open Ppconstr
 
-open Store.Field
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
@@ -638,8 +632,6 @@ let pr_instance_gmap insts =
 open Declarations
 open Termops
 open Reduction
-open Inductive
-open Inductiveops
 
 let print_params env params =
   if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml
index 3c96a41b9..551db10d5 100644
--- a/printing/tactic_printer.ml
+++ b/printing/tactic_printer.ml
@@ -8,8 +8,6 @@
 
 open Pp
 open Errors
-open Util
-open Sign
 open Evd
 open Tacexpr
 open Proof_type