1 files changed, 5 insertions, 38 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..0931c3e61e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,11 +12,9 @@ open Pp
 open Util
 open Names
 open Termops
-open EConstr
 open Environ
 open Genredexpr
 open Tactics
-open Clenv
 open Locus
 open Proofview.Notations
 open Hints
@@ -69,38 +67,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv h gl =
-  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
-  (* [clenv] has been generated by a hint-making function, so the only relevant
-     data in its evarmap is the set of metas. The [evar_reset_evd] function
-     below just replaces the metas of sigma by those coming from the clenv. *)
-  let sigma = Tacmach.New.project gl in
-  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
-  (* Still, we need to update the universes *)
-  let clenv, c =
-    if h.hint_poly then
-      (* Refresh the instance of the hint *)
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let emap c = Vars.subst_univs_level_constr subst c in
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      (* Only metas are mentioning the old universes. *)
-      let clenv = {
-        templval = Evd.map_fl emap clenv.templval;
-        templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas emap evd;
-        env = Proofview.Goal.env gl;
-      } in
-      clenv, emap c
-    else
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
-  in clenv, c
-
-let unify_resolve flags (h : hint) =
-  Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv h gl in
-  Clenv.res_pf ~flags clenv
-  end
+let unify_resolve flags h = Hints.hint_res_pf ~flags h
 
 let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
 
@@ -110,10 +77,10 @@ let unify_resolve_gen = function
 
 let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv h gl in
-    Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-    (exact_check c)
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = Hints.fresh_hint env sigma h in
+    Proofview.Unsafe.tclEVARS sigma <*> exact_check c
   end
 
 (* Util *)