Remove unused [open] statements

19 files changed, 0 insertions, 19 deletions

diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index b014af2c7..eb25994be 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open CClosure
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index e9b3d197b..32da81f96 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Term
-open Termops
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0d741a5a5..c4238e8b0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open EConstr
 open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdf..c26e7458e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,7 +22,6 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
-open Typeops
 open Pretype_errors
 open Classops
 open Evarutil
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index bc63d092d..ea3d3f0fa 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -8,7 +8,6 @@
 
 open Evd
 open Names
-open Term
 open Environ
 open EConstr
 open Glob_term
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba408679..483e2b432 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Environ
 open EConstr
 open Vars
 open Inductiveops
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4bb66b8e9..305eae15a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -21,7 +21,6 @@ open Recordops
 open Evarutil
 open Evardefine
 open Evarsolve
-open Globnames
 open Evd
 open Pretype_errors
 open Sigma.Notations
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fc07f0fbe..7cee1e8a7 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open Reductionops
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c5ae684e3..5fd104c78 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index e3d3b74f1..d22f94e4e 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Locus
-open Term
 open Evd
 open Pretype_errors
 open Environ
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5b42add28..429e5005e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d04495..33a68589c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -20,7 +20,6 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 open Pattern
-open Evd
 open Environ
 
 let case_info_pattern_eq i1 i2 =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5694d345c..791fd74ed 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Globnames
 open Glob_term
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 24f6d1689..f9cf6b83b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 497bde340..68ef97659 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,7 +33,6 @@ open EConstr
 open Vars
 open Reductionops
 open Type_errors
-open Typeops
 open Typing
 open Globnames
 open Nameops
diff --git a/pretyping/program.ml b/pretyping/program.ml
index caa5a5c8a..42acc5705 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 76d0bc241..c31212e26 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open Evd
 open EConstr
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2db0e9e88..754dacd19 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9bd430e4d..558575ccc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr