Merge PR#582: Fix warnings

21 files changed, 5 insertions, 35 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42230dff1..c2d12ebd0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,16 +10,12 @@ module CVars = Vars
 
 open Pp
 open Util
-open CErrors
 open Names
-open Vars
 open Termops
 open EConstr
 open Environ
-open Tacmach
 open Genredexpr
 open Tactics
-open Tacticals
 open Clenv
 open Locus
 open Proofview.Notations
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e347..9ed9f0ae2 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 2a5e7c345..27f624f71 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 54e4405d1..2d6dffdd2 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,9 +18,7 @@ open Names
 open Term
 open Termops
 open EConstr
-open Reduction
 open Proof_type
-open Tacticals
 open Tacmach
 open Tactics
 open Clenv
@@ -357,12 +355,12 @@ let shelve_dependencies gls =
 
 let hintmap_of sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none secvars db
+  | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
      fun db ->
      if Hint_db.use_dn db then (* Using dnet *)
-       Hint_db.map_eauto sigma secvars hdc concl db
-     else Hint_db.map_existential sigma secvars hdc concl db
+       Hint_db.map_eauto sigma ~secvars hdc concl db
+     else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
@@ -1219,7 +1217,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 +1254,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 738cc0feb..c5731e377 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,9 +9,7 @@
 (** This files implements typeclasses eauto *)
 
 open Names
-open Constr
 open EConstr
-open Tacmach
 
 val catchable : exn -> bool
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0..2cf5a6829 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 e2006ac1e..c952f4e72 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 e37ec6bce..855cb206f 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 dc1af79ba..fb7cc7b83 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 bac3980d2..5012b0ef7 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 25c28cf4a..cc7701ad5 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 5467b4af2..d979c580a 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.ml b/tactics/hints.ml
index bcc068d3d..240178c9a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) =
 let pr_hint_list_for_head c =
   let dbs = current_db () in
   let validate (name, db) =
-    let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
     (name, db, hints)
   in
   let valid_dbs = List.map validate dbs in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d5..3a0339ff5 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.ml b/tactics/hipattern.ml
index 851554b83..15b40b42d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 let meta3 = mkmeta 3
-let meta4 = mkmeta 4
 
 let op2bool = function Some _ -> true | None -> false
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d..82a3d47b5 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 904a17417..266cac5c7 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 446a62f6d..5835e763d 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 26d4ac994..a343fc81a 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 4173f8734..211a7338b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5040,10 +5040,6 @@ end
 
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
-  open Proofview.Notations
-
-  let exact_proof c = exact_proof c
-
   open Genredexpr
   open Locus
 
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 2c863c42a..726fd23b6 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -49,7 +49,7 @@ struct
     | DNil
 
   (* debug *)
-  let pr_dconstr f : 'a t -> std_ppcmds = function
+  let _pr_dconstr f : 'a t -> std_ppcmds = function
     | DRel -> str "*"
     | DSort -> str "Sort"
     | DRef _ -> str "Ref"