diff options
| author | Pierre-Marie Pédrot | 2017-01-20 10:55:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-01-20 13:51:50 +0100 |
| commit | a9b76df171ceea443885bb4be919ea586a82beee (patch) | |
| tree | 59ed773cbc4846fddf1156a7f9f6fb53a2ef6ae7 /stm | |
| parent | 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (diff) | |
Do not add redundant side effects in tactic code.
This was observable in long proofs, because side effects kept being
duplicated, leading to an additional cost linear in the size of the proof.
This commit touches kernel files, but the corresponding API is only used
in tactic-facing code so that the side_effects type remains opaque. Thus
it does not affect the kernel safety.
Diffstat (limited to 'stm')
0 files changed, 0 insertions, 0 deletions