Removing opens to Clenvtac to track its use more easily.

3 files changed, 9 insertions, 12 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcf954668d..81f133ddc3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -34,7 +34,6 @@ open Coqlib
 open Declarations
 open Indrec
 open Clenv
-open Clenvtac
 open Evd
 open Ind_tables
 open Eqschemes
@@ -147,7 +146,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
-    clenv_pose_dependent_evars true {eqclause with evd = evd'}
+    Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
   let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in
   let occs =
@@ -892,7 +891,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
-  let pf = clenv_value_cast_meta absurd_clause in
+  let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
   Proofview.V82.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (cut_intro absurd_term)
@@ -918,7 +917,7 @@ let onEquality with_evars tac (c,lbindc) =
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
-  let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
+  let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
@@ -1263,7 +1262,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.e_type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
-      let pf = clenv_value_cast_meta inj_clause in
+      let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
 	evdref := sigma;
 	Some (pf, ty)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f647ac510d..4d6893f1c4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,6 @@ open Context
 open Declarations
 open Tacmach
 open Clenv
-open Clenvtac
 open Misctypes
 
 (************************************************************************)
@@ -593,7 +592,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Proofview.V82.tactic (clenv_refine false clenv'))
+      (Proofview.V82.tactic (Clenvtac.clenv_refine false clenv'))
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f65f295b21..1a3e84a1ff 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -28,7 +28,6 @@ open Genredexpr
 open Tacmach
 open Logic
 open Clenv
-open Clenvtac
 open Refiner
 open Tacticals
 open Hipattern
@@ -793,7 +792,7 @@ let check_unresolved_evars_of_metas clenv =
    [id] is replaced by P using the proof given by [tac] *)
 
 let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl =
-  let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
   let clenv =
     if with_classes then
       { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
@@ -844,7 +843,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty,
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  res_pf elimclause' ~with_evars:with_evars ~flags gl
+  Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags gl
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -3230,7 +3229,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
   let elimclause' = recolle_clenv nparams indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  clenv_refine with_evars resolved gl
+  Clenvtac.clenv_refine with_evars resolved gl
 
 (* Apply induction "in place" replacing the hypothesis on which
    induction applies with the induction hypotheses *)
@@ -3587,7 +3586,7 @@ let elim_scheme_type elim t gl =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
-	res_pf clause' ~flags:(elim_flags ()) gl
+	Clenvtac.res_pf clause' ~flags:(elim_flags ()) gl
     | _ -> anomaly (Pp.str "elim_scheme_type")
 
 let elim_type t gl =