diff options
| -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() ++ |