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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/auto.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 2d92387c03..647ff97148 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 |