From 9a1bbeee7712f21d55cc352020ff51203cac7c51 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 17 Dec 2014 10:24:31 +0100
Subject: CoqIDE: better messages

---
 ide/coqOps.ml | 2 +-
 ide/coqide.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 63b6bf1406..a62cbce73d 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -539,7 +539,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Pp.Info "Doc checked";
+         messages#push Pp.Info "All proof terms checked by the kernel";
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c96a34018a..20542eb764 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1106,7 +1106,7 @@ let build_ui () =
       ~tooltip:"Next occurence"
       ~accel:(prefs.modifier_for_navigation^"greater");
     item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
-      ~tooltip:"Force the processing of the whole document" 
+      ~tooltip:"Fully check the document" 
       ~accel:(current.modifier_for_navigation^"f"); 
   ];
 
-- 
cgit v1.2.3