Merge Clenvtac into Clenv.

Having two different modules led to the availability of internal API in
the mli.

6 files changed, 16 insertions, 16 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4f7bb7ee1e..3287c1c354 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,7 +99,7 @@ let connect_hint_clenv h gl =
 let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv h gl in
-  Clenvtac.res_pf ~flags clenv
+  Clenv.res_pf ~flags clenv
   end
 
 let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 56d6f7f09a..5ad21c2a5b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -158,17 +158,17 @@ let e_give_exact flags h =
   in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
   Proofview.Unsafe.tclEVARS sigma <*>
-  Clenvtac.unify ~flags t1 <*> exact_no_check c
+  Clenv.unify ~flags t1 <*> exact_no_check c
   end
 
 let unify_e_resolve flags = begin fun gls (h, _) ->
   let clenv', c = connect_hint_clenv h gls in
-  Clenvtac.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
+  Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
   end
 
 let unify_resolve flags = begin fun gls (h, _) ->
   let clenv', _ = connect_hint_clenv h gls in
-  Clenvtac.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
+  Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7269228485..d275e15255 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -37,7 +37,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   if occur_existential sigma t1 || occur_existential sigma t2 then
     Tacticals.New.tclTHENLIST
       [Proofview.Unsafe.tclEVARS sigma;
-       Clenvtac.unify ~flags t1;
+       Clenv.unify ~flags t1;
        exact_no_check c]
   else exact_check c
   end
@@ -68,7 +68,7 @@ open Auto
 let unify_e_resolve flags h =
   Proofview.Goal.enter begin fun gl ->
       let clenv', c = connect_hint_clenv h gl in
-      Clenvtac.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
+      Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
     end
 
 let hintmap_of sigma secvars concl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 79b6dfe920..39017c946f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,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') =
-    Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+    Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
   in
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
@@ -1045,7 +1045,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
     let pf_ty = mkArrow eqn Sorts.Relevant false_0 in
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
-    let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
+    let pf = Clenv.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous false_0)
       [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
@@ -1067,7 +1067,7 @@ let onEquality with_evars tac (c,lbindc) =
   let t = pf_get_type_of gl 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' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
+  let eq_clause' = Clenv.clenv_pose_dependent_evars ~with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   (* FIXME evar leak *)
   let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
@@ -1397,7 +1397,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.type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
-      let pf = Clenvtac.clenv_value_cast_meta inj_clause in
+      let pf = Clenv.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 483d8a726b..22c5bbe73f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -695,7 +695,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Clenvtac.res_pf ~flags elimclause')
+      (Clenv.res_pf ~flags elimclause')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end) end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fd9fd81500..3133f9be1e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1373,7 +1373,7 @@ let do_replace id = function
    [id] is replaced by P using the proof given by [tac] *)
 
 let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
-  let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
+  let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
   let clenv =
       { clenv with evd = Typeclasses.resolve_typeclasses
           ~fail:(not with_evars) clenv.env clenv.evd }
@@ -1475,7 +1475,7 @@ let general_elim_clause with_evars flags where indclause elim =
   match where with
   | None ->
     let elimclause = clenv_fchain ~flags indmv elimclause indclause in
-    Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags
+    Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags
   | Some id ->
     let hypmv =
       match List.remove Int.equal indmv (clenv_independent elimclause) with
@@ -1737,7 +1737,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
         let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
         if n<0 then error "Applied theorem does not have enough premises.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
-        Clenvtac.res_pf clause ~with_evars ~flags
+        Clenv.res_pf clause ~with_evars ~flags
       with exn when noncritical exn ->
         let exn, info = Exninfo.capture exn in
         Proofview.tclZERO ~info exn
@@ -4371,7 +4371,7 @@ let induction_tac with_evars params indvars elim =
   (* elimclause' is built from elimclause by instantiating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
-  Clenvtac.res_pf ~with_evars ~flags:(elim_flags ()) elimclause'
+  Clenv.res_pf ~with_evars ~flags:(elim_flags ()) elimclause'
   end
 
 (* Apply induction "in place" taking into account dependent
@@ -4812,7 +4812,7 @@ let elim_scheme_type elim t =
           (* t is inductive, then CUMUL or CONV is irrelevant *)
           clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
-        Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
+        Clenv.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
     | _ -> anomaly (Pp.str "elim_scheme_type.")
   end