diff options
| author | Pierre-Marie Pédrot | 2014-06-17 15:51:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-17 17:08:30 +0200 |
| commit | b5ed27b9b8043e3df3ee4cd918f93fbf7465285f (patch) | |
| tree | 5facb7bad17b086bd0a29cbc219f2aac30865107 /kernel/kernel.mllib | |
| parent | 4e0e3022ca9eefefb57632152725b4a4c249ce38 (diff) | |
Tentative optimization not to nf_evar too often in the compatibility
layer. To this intent, we add a cache evar_map in goals that is the
latest known one where the goal is nf-evarized. If the current one
and the cache coincide, we leave the goal as-is.
Diffstat (limited to 'kernel/kernel.mllib')
0 files changed, 0 insertions, 0 deletions