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

1 files changed, 1 insertions, 9 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 1e4ef4709..d51174a42 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