Remove unused [open] statements

18 files changed, 0 insertions, 22 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42230dff17..324c551d05 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open CErrors
 open Names
-open Vars
 open Termops
 open EConstr
 open Environ
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e3470..9ed9f0ae26 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
 (** This files implements auto and related automation tactics *)
 
 open Names
-open Term
 open EConstr
 open Clenv
 open Pattern
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2a5e7c3458..27f624f716 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Pattern
 open Names
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c430e776a4..6c724a1eb1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,7 +18,6 @@ open Names
 open Term
 open Termops
 open EConstr
-open Reduction
 open Proof_type
 open Tacticals
 open Tacmach
@@ -1219,7 +1218,6 @@ module Search = struct
 
   let intro_tac info kont gl =
     let open Proofview in
-    let open Proofview.Notations in
     let env = Goal.env gl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
@@ -1257,7 +1255,6 @@ module Search = struct
   let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
-    let open Proofview.Notations in
     if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
       Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 738cc0feba..4ab29f260f 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,7 +9,6 @@
 (** This files implements typeclasses eauto *)
 
 open Names
-open Constr
 open EConstr
 open Tacmach
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0a..2cf5a68298 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Misctypes
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2006ac1e3..c952f4e721 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
-open Proof_type
 open Hints
 open Tactypes
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e37ec6bce2..855cb206fe 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open Termops
 open EConstr
 open Inductiveops
diff --git a/tactics/elim.mli b/tactics/elim.mli
index dc1af79ba0..fb7cc7b838 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Tacticals
 open Misctypes
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2b..5012b0ef7f 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -25,7 +25,6 @@ open Constr_matching
 open Misctypes
 open Tactypes
 open Hipattern
-open Pretyping
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 25c28cf4ac..cc7701ad5f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5467b4af25..d979c580aa 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open Evd
 open EConstr
 open Environ
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d53..3a0339ff57 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -9,7 +9,6 @@
 open Pp
 open Util
 open Names
-open Term
 open EConstr
 open Environ
 open Globnames
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d7..82a3d47b59 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Evd
 open EConstr
 open Coqlib
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 904a17417a..266cac5c7d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 446a62f6db..5835e763dd 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Misctypes
 open Tactypes
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 26d4ac994b..a343fc81a7 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Constrexpr
 open Misctypes
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 53f8e4d5fe..f3f7d16b76 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5037,8 +5037,6 @@ end
 
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
-  open Proofview.Notations
-
   open Genredexpr
   open Locus