From 15dd0804812bf457c06f51193ade0b5711668b0d Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 16 Sep 2003 19:17:48 +0000 Subject: Tentative amelioration pretty-printing symboles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4402 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/metasyntax.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c65d0bc73..4df5c8d20 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -230,7 +230,7 @@ let is_right_bracket_on_right s = let is_comma s = let l = String.length s in l <> 0 & - (s.[0] = ',' or s.[0] = ';' or s.[0] = ':') + (s.[0] = ',' or s.[0] = ';') let is_operator s = let l = String.length s in l <> 0 & @@ -459,7 +459,7 @@ let cache_syntax_extension (_,(_,prec,ntn,gr,se,translate)) = warning ("Notation "^ntn^" was already assigned a different level"); raise Not_found end else - error ("Notation "^ntn^" is already assigned a different level") + error ("Notation "^ntn^" is already assigned different level or sublevels") else (* The notation is already declared; no need to redeclare it *) () -- cgit v1.2.3