From 1a2242d6bdeaf53f0856b26e64b4fdbe2ce8fd0a Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Sun, 11 Aug 2013 07:41:21 +0000
Subject: Mutual proofs cannot be delegated

I don't know why yet, but let's be conservative

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16697 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 215162b856..52a5bd4960 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -740,6 +740,8 @@ let collect_proof cur hd id =
     | _, `Alias _ -> collect None (id::accn) view.next
     | Some (parent, (_,_,VernacExactProof _)), `Fork _ ->
         `NotOptimizable `Immediate
+    | _, `Fork(_,_,_::_::_)->
+        `NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
     | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', _) ->
         assert( hd = hd' );
         `Optimizable (parent, Some v, accn)
-- 
cgit v1.2.3