diff options
| author | Maxime Dénès | 2016-11-06 14:26:01 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-07 09:11:46 +0100 |
| commit | 207fcfd9355b01441f2a01614a7de017f4148cde (patch) | |
| tree | 4ae748ce2c1e1b74ab3e46c3f6d616b1c1f271fd | |
| parent | 75b49b14987ec9467ec5916609da8ce3136d3e11 (diff) | |
Improve formatting of a message in [Arguments].
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 86b86e572d..8a28d979c7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1109,11 +1109,11 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags if !rename_flag_required && not rename_flag then errorlabstrm "vernac_declare_arguments" (strbrk "To rename arguments the \"rename\" flag must be specified." - ++ + ++ spc () ++ match !example_renaming with | None -> mt () | Some (o,n) -> - str "\nArgument " ++ pr_name o ++ + str "Argument " ++ pr_name o ++ str " renamed to " ++ pr_name n ++ str "."); let duplicate_names = |