From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index e823373f7b..3738aa94aa 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1380,7 +1380,7 @@ end = struct (* {{{ *)
       if not drop then begin
         let checked_proof = Future.chain ~pure:false future_proof (fun p ->
           let pobject, _ =
-            Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+            Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
           stm_vernac_interp stop
@@ -2432,7 +2432,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       let id = VCS.new_node ?id () in
       VCS.merge id ~ours:(Qed (qed None)) brname;
       VCS.delete_branch brname;
-      VCS.propagate_sideff None;
+      VCS.propagate_sideff ~replay:None;
       `Ok
   | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
       let ofp =
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 stm/stm.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 3738aa94aa..f773d60c55 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1041,13 +1041,6 @@ end = struct (* {{{ *)
         | `Stop x -> x
         | `Cont acc -> next acc
  
-  let back_safe () =
-    let id =
-      fold_until (fun n (id,_,_,_,_) ->
-        if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
-        0 (VCS.get_branch_pos (VCS.current_branch ())) in
-    backto id
-
   let undo_vernac_classifier v =
     try
       match v with
-- 
cgit v1.2.3


From 9be835c4f16b3bc08ff9540a6854ced2d8185cb2 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:09:05 +0200
Subject: Remove unused constructors

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index f773d60c55..8c1185b6dc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1274,7 +1274,6 @@ end = struct (* {{{ *)
     | RespBuiltProof of Proof_global.closed_proof_output * float
     | RespError of error
     | RespStates of (Stateid.t * State.partial_state) list
-    | RespDone
 
   let name = ref "proofworker"
   let extra_env () = !async_proofs_workers_extra_env
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 stm/stm.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.mli b/stm/stm.mli
index 30e9629c6f..d2bee44964 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Vernacexpr
 open Names
-open Feedback
-open Loc
 
 (** state-transaction-machine interface *)
 
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 stm/stm.ml | 3 +++
 stm/vcs.ml | 2 --
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 8c1185b6dc..84c8aa9a99 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1205,6 +1205,8 @@ let detect_proof_block id name =
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
+(* Unused module warning doesn't understand [module rec] *)
+[@@@ocaml.warning "-60"]
 module rec ProofTask : sig
  
   type competence = Stateid.t list
@@ -2318,6 +2320,7 @@ let known_state ?(redefine_qed=false) ~cache id =
   reach ~redefine_qed id
 
 end (* }}} *)
+[@@@ocaml.warning "+60"]
 
 (********************************* STM API ************************************)
 (******************************************************************************)
diff --git a/stm/vcs.ml b/stm/vcs.ml
index d3886464d9..88f860eb69 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -74,8 +74,6 @@ module Dag = Dag.Make(OT)
 
 type id = OT.t
 
-module NodeSet = Dag.NodeSet
-
 module Branch =
 struct
   type t = string
-- 
cgit v1.2.3