aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index ba9ab9672..c7e0810fd 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -559,7 +559,7 @@ object(self)
if Queue.is_empty queue then conclude topstack else
match Queue.pop queue, topstack with
| `Skip(start,stop), [] ->
- logger Pp.Error "You muse close the proof with Qed or Admitted";
+ logger Pp.Error "You must close the proof with Qed or Admitted";
self#discard_command_queue queue;
conclude []
| `Skip(start,stop), (_,s) :: topstack ->