Post-rebase warnings (unused opens and 2 unused values)

15 files changed, 0 insertions, 19 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 00b31ccce..7c5efaea3 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -15,13 +15,11 @@ open Declarations
 open Term
 open EConstr
 open Vars
-open Tacmach
 open Tactics
 open Typing
 open Ccalgo
 open Ccproof
 open Pp
-open CErrors
 open Util
 open Proofview.Notations
 
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 5099d847b..b4bb62be8 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -8,7 +8,6 @@
 (************************************************************************)
 
 open EConstr
-open Proof_type
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ade94e98e..9900792ca 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,7 +12,6 @@ open Term
 open EConstr
 open Vars
 open Termops
-open Tacmach
 open Util
 open Declarations
 open Globnames
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2b624b983..5a1e7c26a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,7 +10,6 @@ open Unify
 open Rules
 open CErrors
 open Util
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e0d2c38a7..86a677007 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 80a7ae2c2..fb2173083 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -8,7 +8,6 @@
 
 open Term
 open EConstr
-open Tacmach
 open Names
 open Globnames
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 59b842c82..2d18b6605 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open CErrors
 open Util
 open Formula
 open Unify
-open Tacmach
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 18d68f54f..6ed251f34 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Formula
-open Tacmach
 open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=Constr.t
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fdcaedab3..ac979bcf8 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,6 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
 open Proofview.Notations
 open Rewrite
 open Stdarg
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9a1615d3f..5630a2d7b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d55350622..2334be966 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -87,7 +87,6 @@ let rec build_lambda sigma vars ctx m = match vars with
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length ctx in
   let pre, suf = List.chop (pred n) ctx in
   let (na, t, suf) = match suf with
   | [] -> assert false
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 324c551d0..c2d12ebd0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,15 +10,12 @@ module CVars = Vars
 
 open Pp
 open Util
-open CErrors
 open Names
 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/class_tactics.ml b/tactics/class_tactics.ml
index 6c724a1eb..2d6dffdd2 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -19,7 +19,6 @@ open Term
 open Termops
 open EConstr
 open Proof_type
-open Tacticals
 open Tacmach
 open Tactics
 open Clenv
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 4ab29f260..c5731e377 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Tacmach
 
 val catchable : exn -> bool
 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e44b585d7..6d9d71a62 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -131,7 +131,6 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
-let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
 let make_body quoter info ?pre_hdr s =
   pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))