From 86b9e40c2e2fd29c747a9f3ad20ebb2701210155 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 14:06:41 +0200 Subject: Adding a missing period in a notation warning. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 176ac3bf6..d3cac1e3e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -425,7 +425,7 @@ let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" (fun (ntn,which_scope) -> str "Notation" ++ spc () ++ str ntn ++ spc () - ++ strbrk "was already used" ++ which_scope) + ++ strbrk "was already used" ++ which_scope ++ str ".") let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in -- cgit v1.2.3