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

1 files changed, 11 insertions, 6 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 1eae14a3a..3457afff1 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -971,7 +971,8 @@ let collect_proof cur hd id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `MaybeOptimizable (parent, accn)
         else `NotOptimizable `TooShort
-    | _, `Sideff se -> collect None (id::accn) view.next
+    | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
+    | _, `Sideff (`Id _) -> `NotOptimizable `NestedProof
     | _ -> `NotOptimizable `Unknown in
  match cur, (VCS.visit id).step with
  | (parent, (_,_,VernacExactProof _)), `Fork _ ->
@@ -981,6 +982,14 @@ let collect_proof cur hd id =
      else if is_defined cur then `NotOptimizable `Transparent
      else collect (Some cur) [] id
 
+let string_of_reason = function
+  | `Transparent -> "Transparent"
+  | `AlreadyEvaluated -> "AlreadyEvaluated"
+  | `TooShort -> "TooShort"
+  | `NestedProof -> "NestedProof"
+  | `Immediate -> "Immediate"
+  | _ -> "Unknown Reason"
+
 let known_state ?(redefine_qed=false) ~cache id =
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -1052,11 +1061,7 @@ let known_state ?(redefine_qed=false) ~cache id =
               ), `Yes
           | `NotOptimizable reason -> (fun () ->
                 prerr_endline ("NotOptimizable " ^ Stateid.to_string id ^ " " ^
-                  match reason with
-                  | `Transparent -> "Transparent"
-                  | `AlreadyEvaluated -> "AlreadyEvaluated"
-                  | `TooShort -> "TooShort"
-                  | _ -> "WTF");
+                  string_of_reason reason);
                 reach eop;
                 begin match keep with
                 | VtKeep ->