diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:51 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:51 +0000 |
| commit | 81cddc53da47e26bb43771e46e9a1ce03de60d60 (patch) | |
| tree | d83ba4af70286e4e53cc00c8685627f144fae8f4 /ide/document.ml | |
| parent | 318f95e2ac69b04619c9aed11605fed62a59770b (diff) | |
STM: a proof with nested proofs cannot be delegated
The reason is that the state gets altered by side effects
by the Qed of inner proofs. This kind of side effects cannot
be reproduced in the slaves easily. And there is no point
in working hard for this corner case.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/document.ml')
0 files changed, 0 insertions, 0 deletions