From 777f0ace3d2458cbe1840dcf3d8f350452721e84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Feb 2015 09:30:53 +0100
Subject: Removing dead code.

---
 stm/lemmas.mli   | 1 -
 stm/texmacspp.ml | 1 -
 2 files changed, 2 deletions(-)

(limited to 'stm')

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/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
-- 
cgit v1.2.3


From 2c0f1eb6f9a6e16b2b4d3a99542df7f49c81f6ea Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 5 Feb 2015 11:22:26 +0100
Subject: Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)

Here nonsensical means a Qed/Defined without a Lemma.
---
 stm/stm.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 7b24685481..05c59720b1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1863,7 +1863,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 +1886,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 +2044,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
-- 
cgit v1.2.3


From 861ec0bdbe8be5e327b5082102c646882cd23383 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 7 Feb 2015 18:40:18 +0100
Subject: STM: tolerate simple side effects in async proofs (Close: 4006)

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 05c59720b1..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((_,_,_,_::_::_), _) ->
-- 
cgit v1.2.3


From 32a295c7390dd40807a2154b54758c61df9b209f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Feb 2015 12:13:22 +0100
Subject: Fix bug #4014.

---
 stm/vio_checking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

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  
-- 
cgit v1.2.3