aboutsummaryrefslogtreecommitdiff
path: root/vernac/declaremods.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/declaremods.ml')
-rw-r--r--vernac/declaremods.ml2
1 files changed, 1 insertions, 1 deletions
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