aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-14 15:58:36 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-14 15:58:36 +0200
commit791f3254cba602672b834ec3484d308db074b684 (patch)
treeb40ebf8ecf72f4c3cdda5e897bc5f73d24fe6b90 /proofs
parent95a7ddee80fef2d499dce36a7e37fc5c6e374018 (diff)
Add documentation for goal selectors.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_global.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index be353b10a..61fe34750 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -678,7 +678,7 @@ let print_goal_selector = function
let parse_goal_selector = function
| "all" -> Vernacexpr.SelectAll
| i ->
- let err_msg = "A selector must be \"all\" or a natural number." in
+ let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
if i < 0 then Errors.error err_msg;