diff options
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/library/lib.ml b/library/lib.ml index fa0a95d366..3172511c26 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -280,7 +280,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_dir dir in if exists then - user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); + user_err ~hdr:"open_module" (Id.print id ++ str " already exists."); add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 15e6d4ef37..95e05556b9 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -216,7 +216,7 @@ let consistency_checks exists dir dirinfo = else if Nametab.exists_dir dir then user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " already exists") + (DirPath.print dir ++ str " already exists.") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 2fe402ff08..bce208df6e 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1845,6 +1845,6 @@ let inCustomEntry : locality_flag * string -> obj = let declare_custom_entry local s = if Egramcoq.exists_custom_entry s then - user_err Pp.(str "Custom entry " ++ str s ++ str " already exists") + user_err Pp.(str "Custom entry " ++ str s ++ str " already exists.") else Lib.add_anonymous_leaf (inCustomEntry (local,s)) |