diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-24 21:04:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:18:49 +0200 |
| commit | 414a30432119bcc878793b33144f671403132f7a (patch) | |
| tree | 3141b746071890d8495ea326b43e6d6eeab4eb20 /vernac/metasyntax.ml | |
| parent | 5db048b7f9cb5d13e44d87a1007ff042eef25fb5 (diff) | |
Quoting notations in incompatible-level error message.
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 38c418ae0..8b042a3ca 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -700,14 +700,14 @@ let pr_level ntn (from,args,typs) = let error_incompatible_level ntn oldprec prec = user_err - (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ + (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") let error_parsing_incompatible_level ntn ntn' oldprec prec = user_err - (str "Notation " ++ str ntn ++ str " relies on a parsing rule for " ++ str ntn' ++ spc() ++ + (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++ str " which is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ |