From 15a23fc7c103ba47d3f5e77853ff515d926573ca Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 10:39:50 +0200
Subject: STM: fix backtrack in presence of nested, immediate, proofs

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

diff --git a/stm/stm.ml b/stm/stm.ml
index 073a6eeb3a..b6c6d41879 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 =
-- 
cgit v1.2.3