Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)

Reviewed-by: ejgallego

1 files changed, 2 insertions, 3 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1a2ebd2..ab388977a5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3205,10 +3205,9 @@ let edit_at ~doc id =
   let vcs = VCS.backup () in
   let on_cur_branch id =
     let rec aux cur =
-      if id = cur then true
-      else match VCS.visit cur with
+      match VCS.visit cur with
       | { step = `Fork _ } -> false
-      | { next } -> aux next in
+      | { next } -> if id = cur then true else aux next in
     aux (VCS.get_branch_pos (VCS.current_branch ())) in
   let rec is_pure_aux id =
     let view = VCS.visit id in