diff options
| author | Maxime Dénès | 2015-11-02 16:39:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-11-02 16:39:03 +0100 |
| commit | 5a5f2b4253b5834e09f43cb36a81ce6f53cc2da3 (patch) | |
| tree | a79d38a8b7c46e96632f76871ecc8f429c975d50 | |
| parent | 4e643d134f02cfa9a73754c3cf48048541324834 (diff) | |
Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.
| -rw-r--r-- | stm/stm.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 89034706a4..14142aa0c5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,12 +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 id = + let rec is_pure_aux id = let view = VCS.visit id in match view.step with - | `Cmd _ -> is_pure view.next + | `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 @@ -2385,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 && is_pure (VCS.visit qed_id).next && 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) -> |