diff options
| author | Pierre-Marie Pédrot | 2020-07-16 23:11:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 2e22662662ebb44a18b8950e3b2876d6787d2d2f (patch) | |
| tree | 159035d364d842445916296c015a73569004fbf0 | |
| parent | e28edfdc3c373af7f5ca4fbd716c8c5753494d5a (diff) | |
Tentatively more efficient implementation of e_give_exact for typeclasses.
The old code was refreshing the whole evarmap when only the constraints
introduced by the term would matter. Since exact hints never introduces
metas for missing binders, there is nothing to extract from the clenv,
so we can just generate a fresh universe substitution.
| -rw-r--r-- | tactics/class_tactics.ml | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 62470a60c0..64d62a89b0 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -143,24 +143,17 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = resolve_evars = false } -let refresh_undefined_univs clenv = - match EConstr.kind clenv.evd clenv.templval.rebus with - | Var _ -> clenv.evd, Univ.empty_level_subst - | App (f, args) when isVar clenv.evd f -> clenv.evd, Univ.empty_level_subst - | _ -> Evd.refresh_undefined_universes clenv.evd - let e_give_exact flags h = - let { hint_term = c; hint_clnv = clenv } = h in + let { hint_term = c; hint_uctx = ctx } = h in let open Tacmach.New in Proofview.Goal.enter begin fun gl -> let sigma = project gl in let c, sigma = if h.hint_poly then - (* Should we really refresh all universes when we have the local ones at hand? *) - let evd, subst = refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true sigma evd in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let evd = Evd.merge_context_set Evd.univ_flexible sigma ctx in let c = Vars.subst_univs_level_constr subst c in - c, evd + c, evd else c, sigma in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in |