From 1a429d34d1cb1f187dd0cc368cd68cb173f93b82 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 18:55:28 +0100
Subject: STM: ease re-editing of Admitted proofs

---
 stm/stm.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 092f8eed1d..70e242bb54 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1010,13 +1010,14 @@ end = struct (* {{{ *)
     match s, t, r with
     | `Old c, States _, RespStates l ->
         List.iter (fun (id,s) -> State.assign id s) l; `End
-    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
               RespBuiltProof (pl, time) ->
         feedback (Feedback.InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time t_name t_loc time;
-        if not !Flags.async_proofs_full then `End
-        else `Stay(t_states,[States t_states])
+        if !Flags.async_proofs_full || t_drop
+        then `Stay(t_states,[States t_states])
+        else `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
         feedback (Feedback.InProgress ~-1);
-- 
cgit v1.2.3