aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-01-27 09:36:47 +0100
committerPierre-Marie Pédrot2016-01-27 09:51:56 +0100
commit22a2cc1897f0d9f568ebfb807673e84f6ada491a (patch)
tree19b995a0acaecd2ffbe299b59e58b5c159ecd86c /dev
parent40cc1067dc5353d43ea2f6643cd8ca954e3e8afa (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 'dev')
0 files changed, 0 insertions, 0 deletions