diff options
| author | Enrico Tassi | 2016-09-06 12:57:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-06 12:57:59 +0200 |
| commit | 5d25643afe3fe0428932e073a23ce3bafb3cb1b1 (patch) | |
| tree | 0c773bbfe82de0178706991913974a332b3ac1b2 /plugins | |
| parent | 6745caadf63630c1ad725402fd527ba592dbcd0e (diff) | |
STM: nested Abort is like nested Qed (fix #4756)
There was an "optimization", since Abort is an empty side effect.
But that optimization had an impact on the DAG shape.
Now a nested proof, no matter if it is kept or dropped, is handled the same.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions