From c6863a4cf8a9ec4bc91335f59f3094974f01dd13 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Sep 2014 09:39:09 +0200
Subject: Fix a message.

---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index bb1c2dab95..b12aea5dbf 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -611,7 +611,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
           | [] , [] , _ ->
 	    (* emacs mode: xml-like flag for detecting information message *)
 	    str (emacs_str "<infomsg>") ++
-	    str "No more, however there are goals you gave up. You need to go back and solve them."
+	    str "No more goals, however there are goals you gave up. You need to go back and solve them."
 	    ++ str (emacs_str "</infomsg>")
 	    ++ fnl () ++ fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
-- 
cgit v1.2.3