From bf6a5e1c7b10d6ff5686cc4a3e71eb105d7a0473 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 22:15:33 +0100
Subject: Missing dot in an error message.

---
 vernac/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index bce208df6e..f9f65a8c30 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1664,7 +1664,7 @@ let add_notation_interpretation env decl_ntn =
       decl_ntn_scope = sc;
     } = decl_ntn in
   match interp_non_syntax_modifiers modifiers with
-  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here")
+  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.")
   | Some (only_parsing,only_printing,entry) ->
     let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in
     Dumpglob.dump_notation (loc,df') sc true
-- 
cgit v1.2.3