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

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