diff options
| author | Maxime Dénès | 2017-09-13 19:19:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-13 19:19:57 +0200 |
| commit | a86bdf0cae05e46d5f0516f29254aeb72bf08de7 (patch) | |
| tree | f45611447003783c5cc5dde40c3a0e268b08325d /interp/notation.ml | |
| parent | cc94172036789cfef28007f59510b7f17df5d45d (diff) | |
| parent | b9106a956c32e1352fcad5f0138a4e3ddee0474c (diff) | |
Merge PR #981: Miscellaneous fixes for notations
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 176ac3bf68..d3cac1e3e9 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 |