From 89c2942352ec5d8d5b9cfe1116376412770cb396 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Sep 2016 17:33:38 +0200
Subject: 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...
---
 stm/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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;
-- 
cgit v1.2.3