Move connect_hint_clenv from Auto to Hints.

1 files changed, 27 insertions, 0 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 386224824f..9fac66515a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1593,3 +1593,30 @@ struct
 
   let repr (h : t) = h.code.obj
 end
+
+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