From 414a30432119bcc878793b33144f671403132f7a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Jul 2017 21:04:36 +0200 Subject: Quoting notations in incompatible-level error message. --- vernac/metasyntax.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/metasyntax.ml') 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() ++ -- cgit v1.2.3