diff options
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | tactics/auto.ml | 38 |
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 |