diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-27 09:36:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-27 09:51:56 +0100 |
| commit | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (patch) | |
| tree | 19b995a0acaecd2ffbe299b59e58b5c159ecd86c | |
| parent | 40cc1067dc5353d43ea2f6643cd8ca954e3e8afa (diff) | |
Fix bug #4537: Coq 8.5 is slower in typeclass resolution.
The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 13 |
3 files changed, 13 insertions, 5 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 01083142b..544114518 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1467,6 +1467,10 @@ let map_metas_fvalue f evd = in set_metas evd (Metamap.smartmap map evd.metas) +let map_metas f evd = + let map cl = map_clb f cl in + set_metas evd (Metamap.smartmap map evd.metas) + let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with | Clval(_,b,_) -> Some b diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 0b4f18536..9cfca02ed 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -455,6 +455,7 @@ val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map +val map_metas : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status diff --git a/tactics/auto.ml b/tactics/auto.ml index 2d92387c0..647ff9714 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -85,11 +85,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = 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, map c + (** Only metas are mentioning the old universes. *) + let clenv = { + templval = Evd.map_fl map clenv.templval; + templtyp = Evd.map_fl map clenv.templtyp; + evd = Evd.map_metas map evd; + env = Proofview.Goal.env gl; + } in + clenv, map c else let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl }, c |