diff options
| author | Pierre-Marie Pédrot | 2017-03-23 09:53:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-23 11:54:48 +0100 |
| commit | 055ff65ac0da60ec76d0f382dab316c3a3302a06 (patch) | |
| tree | ca629d89a4debb3ae30f13da3efe199b49d04da1 /dev | |
| parent | f9526a2bcd05174b7adfe56b7375f0306a2a1e6d (diff) | |
Fast path in computation of frozen evars in Pretyping.
Most of the time, undefined evars are not modified by the considered function,
which leads to the costly recomputation of a trivial partition of evars. We
simply take advantage of physical equality to discriminate when this is
useless and special-case it in the type of frozen evars.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions