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(-)

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