From fc698ea73b9bbf20a12a14f9d6a07eb802a61d27 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 18 Apr 2012 14:35:29 +0000
Subject: Renamed end-of-proof message by a less disturbing one.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15201 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/ideproof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 1e0f526a07..b79d646920 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -125,7 +125,7 @@ let display mode (view:GText.view) goals hints evars =
       in
       List.iter iter evs
     | _ ->
-      view#buffer#insert "Proof Completed."
+      view#buffer#insert "No more subgoals."
     end
   | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
     (* No foreground proofs, but still unfocused ones *)
-- 
cgit v1.2.3