diff options
| author | Enrico Tassi | 2016-09-29 17:33:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-29 17:51:06 +0200 |
| commit | 89c2942352ec5d8d5b9cfe1116376412770cb396 (patch) | |
| tree | b85448594d533362fded55238605db60d8f6faf6 | |
| 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...
| -rw-r--r-- | stm/stm.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index c53bd958aa..bb4f5f72f3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2177,7 +2177,10 @@ let known_state ?(redefine_qed=false) ~cache id = Slaves.build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> reach ~cache:`Shallow start; |