diff options
| author | Pierre-Marie Pédrot | 2020-09-09 11:09:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-10 14:06:47 +0200 |
| commit | 4f5026b1e797e1ed0e501118161052203e1aca50 (patch) | |
| tree | 927d84249ca1c289bb7ae0f7918020670cc1fbd0 /kernel/nativecode.mli | |
| parent | cdfe69d6da6b32338ba74c9f599c74389089c9dd (diff) | |
Add a fast-path to Tactics.e_change_in_hyps.
In case we give an empty list of occurrences to e_change_in_hyps, we
can return immediately. This saves the allocation of a dummy evar, and
a O(n) map over the context for "local" reduction functions.
Note that passing an empty list of hypotheses is the default for both
the "change" tactic and reduction tactics.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions