From d153f3da0dc05d829fb3e0c234b555e170d0c074 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Wed, 4 Jul 2012 11:36:44 +0000
Subject: When focused on an empty list of goal (after finishing a subproof
 introduced by a bullet or a brace, for instance), the message "This subproof
 is complete […]" is now rendered before the list of goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15507 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/printer.ml | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 1e4ef47095..d51174a42f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -431,15 +431,7 @@ let pr_open_subgoals () =
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
             begin match bgoals with
 	    | [] -> pr_subgoals None sigma seeds goals
-	    | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
-		      str"This subproof is complete, but there are still unfocused goals."
-		(* spiwack: to stay compatible with the proof general and coqide,
-		    I use print the message after the goal. It would be better to have
-		    something like:
-		      str"This subproof is complete, but there are still unfocused goals:"
-		      ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
-		    instead. But it doesn't quite work.
-		*)
+	    | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals None bsigma seeds bgoals
 	    end
   | _ -> pr_subgoals None sigma seeds goals
   end
-- 
cgit v1.2.3