diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-07-30 10:39:50 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-07-30 14:35:20 +0200 |
| commit | 15a23fc7c103ba47d3f5e77853ff515d926573ca (patch) | |
| tree | aafb3970c9649fcd150c8092b4cc4e86fabe60ae /stm | |
| parent | 7a370cbd36a63ba8274d5ac0a3b55e0415f33d2c (diff) | |
STM: fix backtrack in presence of nested, immediate, proofs
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 073a6eeb3..b6c6d4187 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2305,9 +2305,7 @@ 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 - | { next } when next = root -> root - | { step = `Fork _ } -> tip - | { step = `Sideff (`Ast(_,id)|`Id id) } -> id + | { step = (`Fork _ | `Sideff _ | `Qed _) } -> 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 = |