From ef21afeec21523a79049e9021712a3f52451cd3a Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Sat, 10 Aug 2013 08:43:04 +0000
Subject: 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
---
 toplevel/stm.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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;
-- 
cgit v1.2.3