Move connect_hint_clenv from Auto to Hints.

1 files changed, 0 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..f485e7f02e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Termops
-open EConstr
 open Environ
 open Genredexpr
 open Tactics
@@ -69,33 +68,6 @@ 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