Change how the number of open goals is printed.

If you are focused on 3 subgoals, and unfocusing would reveal 2 extra
subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop
will tell you:

3 focused subgoals (unfocused: 2-4)

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

1 files changed, 15 insertions, 1 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 27a65da4c..ac61c0648 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -149,12 +149,26 @@ type proof = { (* current proof_state *)
 
 (*** General proof functions ***)
 
+let proof { state = p } =
+  let (goals,sigma) = Proofview.proofview p.proofview in
+  (* spiwack: beware, the bottom of the stack is used by [Proof]
+     internally, and should not be exposed. *)
+  let rec map_minus_one f = function
+    | [] -> assert false
+    | [_] -> []
+    | a::l -> f a :: (map_minus_one f l)
+  in
+  let stack =
+    map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
+  in
+  (goals,stack,sigma)
+
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
 
 (* spiwack: a proof is considered completed even if its still focused, if the focus
-                   doesn't hide any goal.
+   doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
 let is_done p =
   Proofview.finished p.state.proofview &&