From fd9aa81ab6d48f99b461562d7e964a45a5a63b37 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 10 Feb 2014 15:39:46 +0100
Subject: STM: be conservative w.r.t. proofs containing global side effects

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

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index ed420ebbe4..b3835bd307 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1212,8 +1212,7 @@ let collect_proof cur hd brkind id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check () then `MaybeASync (parent, accn, ids)
         else `Sync `Policy
-    | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
-    | _, `Sideff (`Id _) -> `Sync `NestedProof
+    | _, `Sideff _ -> `Sync `NestedProof
     | _ -> `Sync `Unknown in
  match cur, (VCS.visit id).step, brkind with
  |( parent, { expr = VernacExactProof _ }), `Fork _, _ ->
-- 
cgit v1.2.3