Fixing perfomance issue of auto hints induced by universes.

Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.

2 files changed, 27 insertions, 13 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..059c812ad5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
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