diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-29 17:33:38 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-29 17:51:06 +0200 |
| commit | 89c2942352ec5d8d5b9cfe1116376412770cb396 (patch) | |
| tree | b85448594d533362fded55238605db60d8f6faf6 /.gitignore | |
| parent | 601fd9343a241706c0a205aaf8e08255753c3780 (diff) | |
STM: compute the correct state for edited Qed (#5086)
When a proof is 're-opened', the Qed node does not change.
Still the STM has to install the old state (where only
the future proof has to be updated). This bit was missing.
Why was it working: the bug happens only if you
reopen the very last proof, i.e. there is no
sentence that stays valid after the Qed. If there
is such a sentence, its state was computed correctly
before, and is not changed. If it is the very last,
then the next state is based on the wrong one...
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions