1 files changed, 42 insertions, 0 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 58bebe319b..41b200bb83 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1599,3 +1599,45 @@ struct
 
   let repr (h : t) = h.code.obj
 end
+
+let connect_hint_clenv h gl =
+  let { 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 *)
+  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. *)
+    {
+      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;
+    }
+  else
+    let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+
+let fresh_hint env sigma h =
+  let { hint_term = c; hint_uctx = ctx } = h in
+  if h.hint_poly then
+    (* Refresh the instance of the hint *)
+    let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+    let c = Vars.subst_univs_level_constr subst c in
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
+  else
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
+
+let hint_res_pf ?with_evars ?with_classes ?flags h =
+  Proofview.Goal.enter begin fun gl ->
+    let clenv = connect_hint_clenv h gl in
+    Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+  end