Removing dead code and unused opens.

9 files changed, 1 insertions, 36 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 6c02a7202f..8b5f527cd0 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -13,14 +13,9 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
-open Stdarg
 open Constrarg
 open Extraargs
-open Pcoq.Constr
-open Pcoq.Prim
-open Pcoq.Tactic
 
-open Proofview.Notations
 open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 79f80260fa..1f3eb13355 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -14,13 +14,11 @@ open Stdarg
 open Constrarg
 open Extraargs
 open Pcoq.Prim
-open Pcoq.Constr
 open Pcoq.Tactic
 open Mod_subst
 open Names
 open Tacexpr
 open Glob_ops
-open Tactics
 open Errors
 open Util
 open Evd
@@ -128,7 +126,6 @@ TACTIC EXTEND ediscriminate
     [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
-open Proofview.Notations
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
   discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
@@ -458,8 +455,6 @@ TACTIC EXTEND evar
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
-open Tacticals
-
 TACTIC EXTEND instantiate
   [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
     [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ]
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 9ef1545416..77075ec4c4 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -10,8 +10,6 @@
 
 open Misctypes
 open Class_tactics
-open Pcoq.Prim
-open Pcoq.Constr
 open Pcoq.Tactic
 open Stdarg
 open Constrarg
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index df499a2c9c..1bbdb17790 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -307,7 +307,6 @@ GEXTEND Gram
   ;
   END
 
-open Stdarg
 open Constrarg
 open Vernacexpr
 open Vernac_classifier
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index f2dbb5b6c9..39db6268b5 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -7,11 +7,9 @@
 (************************************************************************)
 
 open Util
-open Genarg
 open Pp
 open Names
 open Tacexpr
-open Geninterp
 
 (** Tactic notations (TacAlias) *)
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 977c56f38b..3744449e97 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -475,9 +475,6 @@ let clause_app f = function
   | { onhyps=Some l; concl_occs=nl } ->
       { onhyps=Some(List.map f l); concl_occs=nl}
 
-let map_raw wit f ist x =
-  in_gen (glbwit wit) (f ist (out_gen (rawwit wit) x))
-
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
   match (x:raw_atomic_tactic_expr) with
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 31bccd019d..6a5d1380d6 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -21,7 +21,6 @@ open Libnames
 open Globnames
 open Nametab
 open Pfedit
-open Proof_type
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -35,8 +34,6 @@ open Stdarg
 open Constrarg
 open Printer
 open Pretyping
-module Monad_ = Monad
-open Evd
 open Misctypes
 open Locus
 open Tacintern
@@ -196,7 +193,7 @@ module Value = struct
   | OptArg t -> Val.Opt (tag_of_arg t)
   | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
 
-  let rec val_cast arg v = prj (tag_of_arg arg) v
+  let val_cast arg v = prj (tag_of_arg arg) v
 
   let cast (Topwit wit) v = val_cast wit v
 
@@ -695,13 +692,6 @@ let pf_interp_casted_constr ist gl c =
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
 
-let new_interp_constr ist c k =
-  let open Proofview in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let (sigma, c) = interp_constr ist (Goal.env gl) (project gl) c in
-    Sigma.Unsafe.of_pair (k c, sigma)
-  end }
-
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
@@ -1290,7 +1280,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
   | TacML (loc,opn,l) ->
-      let open Ftactic.Notations in
       let trace = push_trace (loc,LtacMLCall tac) ist in
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       let tac = Tacenv.interp_ml_tactic opn in
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 54d32f2666..1326818fc8 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -16,7 +16,6 @@ open Globnames
 open Term
 open Genredexpr
 open Patternops
-open Pretyping
 
 (** Substitution of tactics at module closing time *)
 
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 7cda8d9147..655bfd5f52 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -10,17 +10,12 @@ open Term
 open Hipattern
 open Names
 open Pp
-open Genarg
 open Geninterp
-open Stdarg
 open Misctypes
 open Tacexpr
 open Tacinterp
-open Tactics
-open Errors
 open Util
 open Tacticals.New
-open Proofview.Notations
 
 let tauto_plugin = "tauto"
 let () = Mltop.add_known_module tauto_plugin