diff options
| -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 = |