aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 10:24:31 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commit9a1bbeee7712f21d55cc352020ff51203cac7c51 (patch)
treeba5ba630c8bd6967b1269d6c6ecdfae5d2d18807 /ide
parentc854f859115add2ed95e2e4df36bce2eb2e6f22a (diff)
CoqIDE: better messages
Diffstat (limited to 'ide')
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/coqide.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 63b6bf140..a62cbce73 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 c96a34018..20542eb76 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");
];