diff options
| author | Pierre-Marie Pédrot | 2020-07-16 23:11:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 2e22662662ebb44a18b8950e3b2876d6787d2d2f (patch) | |
| tree | 159035d364d842445916296c015a73569004fbf0 /engine/uState.ml | |
| parent | e28edfdc3c373af7f5ca4fbd716c8c5753494d5a (diff) | |
Tentatively more efficient implementation of e_give_exact for typeclasses.
The old code was refreshing the whole evarmap when only the constraints
introduced by the term would matter. Since exact hints never introduces
metas for missing binders, there is nothing to extract from the clenv,
so we can just generate a fresh universe substitution.
Diffstat (limited to 'engine/uState.ml')
0 files changed, 0 insertions, 0 deletions