diff options
| author | Pierre-Marie Pédrot | 2015-10-14 12:16:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-14 18:48:56 +0200 |
| commit | a895b2c0caf8ec9c0deb04b8dea890283bd7329d (patch) | |
| tree | 2894217b0404d4869e1421205851d2612196b7bb /kernel | |
| parent | bf0499bc507d5a39c3d5e3bf1f69191339270729 (diff) | |
Fixing perfomance issue of auto hints induced by universes.
Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions