Merge Clenvtac into Clenv.

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

1 files changed, 3 insertions, 3 deletions

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] *)