From c30c352b3d7c2a93aea45fedbdc9a7327d743a9f Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 18 Oct 2013 13:52:03 +0000
Subject: STM: not optimize proofs containing an Undo

Actually we could, but we should check the state one jumps to is
inside the proof...

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

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 7086ff722c..789b56914f 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1014,7 +1014,7 @@ let collect_proof cur hd id =
     let view = VCS.visit id in
     match last, view.step with
     | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
-    | _, `Alias _ -> collect None (id::accn) view.next
+    | _, `Alias _ -> `NotOptimizable `Alias
     | _, `Fork(_,_,_::_::_)->
         `NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
     | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', _) ->
@@ -1042,6 +1042,7 @@ let string_of_reason = function
   | `TooShort -> "TooShort"
   | `NestedProof -> "NestedProof"
   | `Immediate -> "Immediate"
+  | `Alias -> "Alias"
   | _ -> "Unknown Reason"
 
 let known_state ?(redefine_qed=false) ~cache id =
-- 
cgit v1.2.3