diff options
| author | Pierre-Marie Pédrot | 2019-02-04 12:16:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 12:16:59 +0100 |
| commit | 019123cf911949480d300beba30b63db19c46b7b (patch) | |
| tree | fd61ecc206db85b0a03eb3c29428b73e5a3f962c | |
| parent | a5f260d6a397706fa91d2e128e9999d0c74b5739 (diff) | |
| parent | 9b39f65b25ff434cddda9a312eb40e9f099d298e (diff) | |
Merge PR #9461: Fix default goal selector error message.
Reviewed-by: ppedrot
| -rw-r--r-- | proofs/goal_select.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index cef3fd3f5e..955d797227 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -45,7 +45,7 @@ let parse_goal_selector = function | "!" -> SelectAlreadyFocused | "all" -> SelectAll | i -> - let err_msg = "The default 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 CErrors.user_err Pp.(str err_msg); |