From 7a370cbd36a63ba8274d5ac0a3b55e0415f33d2c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 10:16:59 +0200
Subject: STM: remove assertion not being true for nested, immediate, proofs
 (#4313)

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 9e82dd156d..073a6eeb3a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1837,7 +1837,6 @@ let known_state ?(redefine_qed=false) ~cache id =
                 Proof_global.discard_all ()
               ), (if redefine_qed then `No else `Yes), true
           | `Sync (name, _, `Immediate) -> (fun () -> 
-                assert (Stateid.equal view.next eop);
                 reach eop; vernac_interp id x; Proof_global.discard_all ()
               ), `Yes, true
           | `Sync (name, pua, reason) -> (fun () ->
-- 
cgit v1.2.3


From 15a23fc7c103ba47d3f5e77853ff515d926573ca Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 10:39:50 +0200
Subject: STM: fix backtrack in presence of nested, immediate, proofs

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 073a6eeb3a..b6c6d41879 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2305,9 +2305,7 @@ let edit_at id =
   let rec master_for_br root tip =
       if Stateid.equal tip Stateid.initial then tip else
       match VCS.visit tip with
-      | { next } when next = root -> root
-      | { step = `Fork _ } -> tip
-      | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
+      | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =
     let master_id, cancel_switch, keep =
-- 
cgit v1.2.3


From 5d0ff1782ab54914e7b0e5a736922aa297d327c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 10:41:13 +0200
Subject: STM: emit a warning when a QED/Admitted proof contains a nested lemma

---
 stm/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index b6c6d41879..ee12e48d5d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1688,7 +1688,10 @@ let collect_proof keep cur hd brkind id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
         `MaybeASync (parent last, None, accn, name, delegate name)
-    | `Sideff _ -> `Sync (no_name,None,`NestedProof)
+    | `Sideff _ ->
+        Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
+           "stop working in the next Coq version")));
+        `Sync (no_name,None,`NestedProof)
     | _ -> `Sync (no_name,None,`Unknown) in
  let make_sync why = function
    | `Sync(name,pua,_) -> `Sync (name,pua,why)
-- 
cgit v1.2.3


From 63ecb7386ae6e705d3f5577e01ec543f706c9427 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 14:35:15 +0200
Subject: STM: make multiple, admitted, nested proofs work (fix #4314)

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

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index ee12e48d5d..bf91c3aa4f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1858,9 +1858,8 @@ let known_state ?(redefine_qed=false) ~cache id =
                       Some(Proof_global.close_proof
                                 ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
-                reach view.next;
-                if keep == VtKeepAsAxiom then
-                  Option.iter (vernac_interp id) pua;
+                if keep != VtKeepAsAxiom then
+                  reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
                 vernac_interp id ?proof x;
                 let wall_clock3 = Unix.gettimeofday () in
-- 
cgit v1.2.3