Stores bullet stack on locally at the level of focuses rather than globally in the proof.

Fixes bug #2568 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2568 )

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14274 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 12 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a5e19e306..a32749073 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -334,12 +334,12 @@ module Bullet = struct
 
   module Strict = struct
     (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
-    let bullet_kind = Proof.new_focus_kind () 
+    let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
     let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
-    let (get_bullets,set_bullets) =
-      let bullets = Store.field () in
-      begin fun pr -> Option.default [] (bullets.get (Proof.get_proof_info pr)) end ,
-      begin fun bs pr -> Proof.set_proof_info (bullets.set bs (Proof.get_proof_info pr)) pr end
+
+    let get_bullets pr =
+      try Proof.get_at_focus bullet_kind pr
+      with Proof.NoSuchFocus -> []
 
     let has_bullet bul pr =
       let rec has_bullet = function
@@ -352,15 +352,13 @@ module Bullet = struct
     (* precondition: the stack is not empty *)
     let pop pr =
       match get_bullets pr with
-      | b::stk -> 
-	Proof.unfocus bullet_kind pr ;
-	set_bullets stk pr ;
-	b
-      | [] -> Util.anomaly "Tried to pop bullet from an empty stack"
+      | b::_ ->
+	Proof.unfocus bullet_kind pr;
+	(*returns*) b
+      | _ -> assert false
 
     let push b pr =
-      Proof.focus bullet_cond () 1 pr ;
-      set_bullets (b::get_bullets pr) pr
+      Proof.focus bullet_cond (b::get_bullets pr) 1 pr
 
     let put p bul =
       if has_bullet bul p then