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

1 files changed, 5 insertions, 1 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 6b4c46d4ec..d033953bd8 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -730,6 +730,9 @@ end = struct (* {{{ *)
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
 let collect_proof cur hd id =
+ let is_defined = function
+   | _, (_, _, VernacEndProof (Proved (false,_))) -> true
+   | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match last, view.step with
@@ -746,6 +749,7 @@ let collect_proof cur hd id =
     | _, `Sideff se -> collect None (id::accn) view.next
     | _ -> `NotOptimizable `Unknown in
  if State.is_cached id then `NotOptimizable `Unknown
+ else if is_defined cur then `NotOptimizable `Transparent
  else collect (Some cur) [] id
 
 let known_state ~cache id =
@@ -802,7 +806,7 @@ let known_state ~cache id =
                  Proof_global.discard_all ())
            | `NotOptimizable `Immediate -> assert (view.next = eop);
                (fun () -> reach eop; interp id x; Proof_global.discard_all ())
-           | `NotOptimizable `Unknown ->
+           | `NotOptimizable _ ->
                (fun () ->
                  prerr_endline ("NotOptimizable " ^ string_of_state_id id);
                  reach eop;