Merge branch 'v8.5'

1 files changed, 15 insertions, 2 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 0c0bdc8272..6236297459 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2317,6 +2317,17 @@ let edit_at id =
       | { step = `Fork _ } -> false
       | { next } -> aux next in
     aux (VCS.get_branch_pos (VCS.current_branch ())) in
+  let rec is_pure_aux id =
+    let view = VCS.visit id in
+    match view.step with
+    | `Cmd _ -> is_pure_aux view.next
+    | `Fork _ -> true
+    | _ -> false in
+  let is_pure id =
+    match (VCS.visit id).step with
+    | `Qed (_,last_step) -> is_pure_aux last_step
+    | _ -> assert false
+  in
   let is_ancestor_of_cur_branch id =
     Vcs_.NodeSet.mem id
       (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
@@ -2327,7 +2338,9 @@ let edit_at id =
   let rec master_for_br root tip =
       if Stateid.equal tip Stateid.initial then tip else
       match VCS.visit tip with
-      | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip
+      | { step = (`Fork _ | `Qed _) } -> tip
+      | { step = `Sideff (`Ast(_,id)) } -> id
+      | { step = `Sideff _ } -> tip
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =
     let master_id, cancel_switch, keep =
@@ -2377,7 +2390,7 @@ let edit_at id =
       | _, Some _, None -> assert false
       | false, Some (qed_id,start), Some(mode,bn) ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch
+          if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
           then reopen_branch start id mode qed_id tip bn
           else backto id (Some bn)
       | true, Some (qed_id,_), Some(mode,bn) ->