From 608bb24403e07e42855311d483e918c7acf3cafb Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 10 Jul 2012 12:40:24 +0000
Subject: 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
---
 printing/printer.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.ml')

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