Merge branch 'v8.5'

4 files changed, 6 insertions, 6 deletions

diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index d0669d7a3e..a0ddd265cb 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -10,7 +10,6 @@ open Names
 open Term
 open Decl_kinds
 open Constrexpr
-open Tacexpr
 open Vernacexpr
 open Pfedit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 7b24685481..3a57d85bab 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1580,6 +1580,7 @@ let collect_proof keep cur hd brkind id =
     let view = VCS.visit id in
     match view.step with
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
     | `Alias _ -> `Sync (no_name,None,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
@@ -1863,7 +1864,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
-let merge_proof_branch ?id qast keep brname =
+let merge_proof_branch ?valid ?id qast keep brname =
   let brinfo = VCS.get_branch brname in
   let qed fproof = { qast; keep; brname; brinfo; fproof } in
   match brinfo with
@@ -1886,7 +1887,7 @@ let merge_proof_branch ?id qast keep brname =
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+       iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
@@ -2044,7 +2045,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
-          let rc = merge_proof_branch ~id:newtip x keep head in
+          let valid = if tty then Some(VCS.get_branch_pos head) else None in
+          let rc = merge_proof_branch ?valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish ();
           rc
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index d71c169d62..a0979f8b15 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -15,7 +15,6 @@ open Bigint
 open Decl_kinds
 open Extend
 open Libnames
-open Flags
 
 let unlock loc =
   let start, stop = Loc.unloc loc in
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 84df3ecd5e..b207222117 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -119,7 +119,7 @@ let schedule_vio_compilation j fs =
   let rec filter_argv b = function
     | [] -> []
     | "-schedule-vio2vo" :: rest -> filter_argv true rest
-    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
     | _ :: rest when b -> filter_argv b rest
     | s :: rest -> s :: filter_argv b rest in
   let prog = Sys.argv.(0) in