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 /kernel/indtypes.ml | |
| 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 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions