aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-12 14:06:41 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-12 20:38:44 +0200
commit86b9e40c2e2fd29c747a9f3ad20ebb2701210155 (patch)
tree3ee3e5367c76a8a506be94a5d49d5d24b3ad658b
parent6c3fd3b8f12eb722d18b5da765bf8aec5e95ee06 (diff)
Adding a missing period in a notation warning.
-rw-r--r--interp/notation.ml2
1 files changed, 1 insertions, 1 deletions
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