diff options
| author | Enrico Tassi | 2014-02-10 15:39:46 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-02-10 18:04:10 +0100 |
| commit | fd9aa81ab6d48f99b461562d7e964a45a5a63b37 (patch) | |
| tree | 4a2557c60b8ce349b24b94a45abb2c6185e6385b | |
| parent | 41845e6d4334eeaa7addf6b11f6cb4cda5a7f8cc (diff) | |
STM: be conservative w.r.t. proofs containing global side effects
| -rw-r--r-- | toplevel/stm.ml | 3 |
1 files changed, 1 insertions, 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 _, _ -> |