Merge PR #6968: [stm] Never consider `Backtrack` as part of the script.

1 files changed, 5 insertions, 0 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ad94b68077..dbecbdae54 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2803,6 +2803,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       (* Meta *)
       | VtMeta, _ ->
         let id, w = Backtrack.undo_vernac_classifier expr in
+        (* Special case Backtrack, as it is never part of a script. See #6240 *)
+        let part_of_script = begin match Vernacprop.under_control expr with
+          | VernacBacktrack _ -> false
+          | _ -> part_of_script
+        end in
         process_back_meta_command ~part_of_script ~newtip ~head id x w
       (* Query *)
       | VtQuery (false,route), VtNow ->