diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 15:58:36 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 15:58:36 +0200 |
| commit | 791f3254cba602672b834ec3484d308db074b684 (patch) | |
| tree | b40ebf8ecf72f4c3cdda5e897bc5f73d24fe6b90 /proofs/proof_global.ml | |
| parent | 95a7ddee80fef2d499dce36a7e37fc5c6e374018 (diff) | |
Add documentation for goal selectors.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 2 |
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; |