1 files changed, 26 insertions, 12 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 72c28ce323..617c491c35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,21 +72,35 @@ let auto_flags_of_state st =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve_nodelta poly (c,clenv) =
+let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.nf_enter begin fun gl ->
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
-  let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in
-  Clenvtac.clenv_refine false clenv''
+  (** [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 = Proofview.Goal.sigma 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 (_, _, ctx) = c in
+  let clenv =
+    if poly then
+      (** Refresh the instance of the hint *)
+      let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+      let map c = Vars.subst_univs_level_constr subst c in
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in
+      (** FIXME: We're being inefficient here because we substitute the whole
+          evar map instead of just its metas, which are the only ones
+          mentioning the old universes. *)
+      Clenv.map_clenv map clenv
+    else
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }
+  in
+  let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+  Clenvtac.clenv_refine false clenv
   end
 
-let unify_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
-  let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in
-  Clenvtac.clenv_refine false clenv''
-  end
+let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
 
 let unify_resolve_gen poly = function
   | None -> unify_resolve_nodelta poly