aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-10 08:43:04 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-10 08:43:04 +0000
commitef21afeec21523a79049e9021712a3f52451cd3a (patch)
treeb153220c82a2ab2ada21a2418103cae3b5765608 /lib/future.ml
parent70736feb562c19b2892dbd5bdc6727bd731bcab6 (diff)
Lemmas ending with Defined cannot be delegated to slaves
We need the proof object to continue (there is no real dependency tracking so we assume we need it immediately). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16694 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/future.ml')
0 files changed, 0 insertions, 0 deletions