diff options
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 42be4fca71..a6a64f2094 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,6 +2317,12 @@ let edit_at id = | { step = `Fork _ } -> false | { next } -> aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in + let rec is_pure id = + let view = VCS.visit id in + match view.step with + | `Cmd _ -> is_pure view.next + | `Fork _ -> true + | _ -> false in let is_ancestor_of_cur_branch id = Vcs_.NodeSet.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in @@ -2377,7 +2383,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 (VCS.visit qed_id).next && 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) -> |