Small change in the printing of proofs for use by coqide.

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

1 files changed, 1 insertions, 0 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 23e6e277fb..a59800a9c1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -454,6 +454,7 @@ let pr_open_subgoals () =
      [evar_info]-s instead. *)
   let p = Proof_global.give_me_the_proof () in
   let (goals , stack , sigma ) = Proof.proof p in
+  let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in