diff options
| author | Pierre-Marie Pédrot | 2016-01-27 09:36:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-27 09:51:56 +0100 |
| commit | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (patch) | |
| tree | 19b995a0acaecd2ffbe299b59e58b5c159ecd86c /pretyping | |
| 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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 01083142b7..5441145189 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 0b4f185368..9cfca02ed8 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 |