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, 15 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 5cc7f61d97..7abb4dc527 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -10,13 +10,10 @@ open Hipattern
 open Names
 open Term
 open Termops
-open Reductionops
 open Tacmach
-open Errors
 open Util
 open Declarations
 open Globnames
-open Inductiveops
 
 let qflag=ref true
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 58bef84ea3..753fdda720 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,9 +12,7 @@ open Rules
 open Instances
 open Term
 open Tacmach
-open Tactics
 open Tacticals
-open Libnames
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ee1c442650..e3367b4c22 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,11 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Formula
-open Sequent
 open Unify
 open Rules
-open Pp
 open Errors
 open Util
 open Term
@@ -20,7 +17,6 @@ open Tactics
 open Tacticals
 open Termops
 open Reductionops
-open Declarations
 open Formula
 open Sequent
 open Names
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 32c6030d1d..37d9edef86 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -14,7 +14,6 @@ open Tacmach
 open Tactics
 open Tacticals
 open Termops
-open Declarations
 open Formula
 open Sequent
 open Globnames
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7e6f65eaa3..6d00e8d9fb 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open Util
 open Formula
 open Unify
 open Tacmach
-open Names
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index ab18434de2..33ea0ac8a0 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,12 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
-open Formula
-open Tacmach
 open Term
-open Names
 open Termops
 open Reductionops