diff options
| author | coqbot-app[bot] | 2020-11-27 17:04:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-27 17:04:01 +0000 |
| commit | 0501761b95f4fd3e22b93aa6bce8c9f96b88495b (patch) | |
| tree | 672b5f5916402923ac59329f3f068d7d758ecf19 /vernac/comArguments.ml | |
| parent | f733414e59afb37cad41c65b11bc4c817bd137f9 (diff) | |
| parent | ce8569a3713536e510381e4d49d534a447cfe637 (diff) | |
Merge PR #13483: Fix #13283: improved error on `clear implicit` flag
Reviewed-by: Zimmi48
Diffstat (limited to 'vernac/comArguments.ml')
| -rw-r--r-- | vernac/comArguments.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index adf1f42beb..a21af12785 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -223,10 +223,10 @@ let vernac_arguments ~section_local reference args more_implicits flags = | _ -> true in if implicits_specified && clear_implicits_flag then - CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"clear implicits\" flag must be omitted if implicit annotations are given."); if implicits_specified && default_implicits_flag then - CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations."); let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) |