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

2 files changed, 0 insertions, 14 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ccf397eda..9bfebe348 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -15,21 +15,12 @@
 
 open Errors
 open Util
-open Pp
-open Reduction
-open Proof_type
 open Names
 open Nameops
 open Term
-open Declarations
-open Environ
-open Sign
-open Inductive
 open Tacticals
 open Tacmach
-open Evar_refiner
 open Tactics
-open Clenv
 open Logic
 open Libnames
 open Globnames
@@ -193,8 +184,6 @@ let coq_Zopp = lazy (zbase_constant "Z.opp")
 let coq_Zminus = lazy (zbase_constant "Z.sub")
 let coq_Zsucc = lazy (zbase_constant "Z.succ")
 let coq_Zpred = lazy (zbase_constant "Z.pred")
-let coq_Zgt = lazy (zbase_constant "Z.gt")
-let coq_Zle = lazy (zbase_constant "Z.le")
 let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
 let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
 let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
@@ -326,7 +315,6 @@ let coq_iff = lazy (constant "iff")
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-open Closure
 let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
   | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
       EvalConstRef kn
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 6abcc7b6f..800254671 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -17,8 +17,6 @@
 (*   the number of source of numbering.                                   *)
 (**************************************************************************)
 
-open Names
-
 module type INT = sig
   type bigint
   val less_than : bigint -> bigint -> bool