diff options
| author | Pierre-Marie Pédrot | 2020-10-05 16:06:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-07 11:29:43 +0200 |
| commit | 7f75bc30ed18253cd9075422ba485008528213fc (patch) | |
| tree | e2664bf262e47ff7b1133c00fa945d5fbd0f8e30 /kernel/vmlambda.mli | |
| parent | bd57c1a48cca55be374e597e2d89fe619a39c26e (diff) | |
Algorithmically faster implementation of Evarconv.apply_on_subterm.
Instead of repeatedly checking for evars to appear in a term, we perform
the search in one single pass. This slowdown was observed in fiat-crypto.
This is still a naive algorithm though, since we recompute the set of evars
for each subterm. This is thus quadratic.
Diffstat (limited to 'kernel/vmlambda.mli')
0 files changed, 0 insertions, 0 deletions