From 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 Mon Sep 17 00:00:00 2001
From: regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 14 Sep 2012 15:59:23 +0000
Subject: 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
---
 proofs/clenv.ml        |  4 ----
 proofs/clenvtac.ml     | 12 ------------
 proofs/evar_refiner.ml |  4 ----
 proofs/logic.ml        |  6 ------
 proofs/pfedit.ml       |  9 ---------
 proofs/proof_global.ml |  1 -
 proofs/proof_type.ml   |  3 ---
 proofs/refiner.ml      |  6 ------
 proofs/tacmach.ml      |  5 -----
 proofs/tactic_debug.ml |  1 -
 10 files changed, 51 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 20a2ebd06..f3e414126 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -14,19 +14,15 @@ open Nameops
 open Term
 open Termops
 open Namegen
-open Sign
 open Environ
 open Evd
 open Reduction
 open Reductionops
-open Glob_term
-open Pattern
 open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
 open Mod_subst
-open Coercion
 open Misctypes
 
 (* Abbreviations *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 3b188c8d0..d7379c902 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,26 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Errors
-open Util
 open Names
-open Nameops
 open Term
 open Termops
-open Sign
-open Environ
 open Evd
-open Evarutil
-open Proof_type
 open Refiner
 open Logic
 open Reduction
-open Reductionops
 open Tacmach
-open Glob_term
-open Pattern
-open Tacexpr
 open Clenv
 
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0024a5c10..260d6d092 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -7,13 +7,9 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Names
-open Term
 open Evd
 open Evarutil
-open Sign
-open Refiner
 
 (******************************************)
 (* Instantiation of existential variables *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a79485d1e..dcf1e4c73 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -11,21 +11,15 @@ open Errors
 open Util
 open Names
 open Nameops
-open Evd
 open Term
 open Termops
-open Sign
 open Environ
 open Reductionops
-open Inductive
 open Inductiveops
 open Typing
 open Proof_type
-open Typeops
 open Type_errors
 open Retyping
-open Evarutil
-open Tacexpr
 open Misctypes
 
 type refiner_error =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d528e95a8..f7d9446b5 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -7,20 +7,11 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
-open Nameops
-open Sign
-open Term
 open Entries
 open Environ
 open Evd
-open Typing
 open Refiner
-open Tacexpr
-open Proof_type
-open Lib
 
 let refining = Proof_global.there_are_pending_proofs
 let check_no_pending_proofs = Proof_global.check_no_pending_proof
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a3e240c8d..bedf058fc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -314,7 +314,6 @@ let maximal_unfocus k p =
 
 module Bullet = struct
 
-  open Store.Field
 
 
   type t = Vernacexpr.bullet
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index dec7b2b07..4a404b6f3 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -7,12 +7,9 @@
 (************************************************************************)
 
 (*i*)
-open Environ
 open Evd
 open Names
-open Libnames
 open Term
-open Pp
 open Tacexpr
 (* open Decl_expr *)
 open Glob_term
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 4b04374da..910653ddb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -9,14 +9,8 @@
 open Pp
 open Errors
 open Util
-open Term
-open Termops
-open Sign
 open Evd
-open Sign
 open Environ
-open Reductionops
-open Type_errors
 open Proof_type
 open Logic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 85ae41a53..cab124d93 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,12 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Errors
 open Util
 open Names
 open Namegen
-open Sign
 open Term
 open Termops
 open Environ
@@ -23,7 +21,6 @@ open Tacred
 open Proof_type
 open Logic
 open Refiner
-open Tacexpr
 
 let re_sig it gc = { it = it; sigma = gc }
 
@@ -194,8 +191,6 @@ let rename_hyp l       = with_check (rename_hyp_no_check l)
 (* Pretty-printers *)
 
 open Pp
-open Tacexpr
-open Glob_term
 
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 49026cc0b..10ce0e76b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Constrextern
 open Pp
 open Tacexpr
 open Termops
-- 
cgit v1.2.3