diff options
| author | Enrico Tassi | 2015-07-30 10:16:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-30 14:35:20 +0200 |
| commit | 7a370cbd36a63ba8274d5ac0a3b55e0415f33d2c (patch) | |
| tree | 6d8b075e47f33dd4d5d36f576c1f27258218cd91 | |
| parent | 5a6e0088adb4e817133d4d7f5a547fbc23fe7951 (diff) | |
STM: remove assertion not being true for nested, immediate, proofs (#4313)
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 () -> |