diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-16 19:17:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-16 19:17:48 +0000 |
| commit | 15dd0804812bf457c06f51193ade0b5711668b0d (patch) | |
| tree | 91cb117e09c50368accd47f717ef4c5101064ae7 | |
| parent | 571c03b533cfbeabe9140534604feb7cb8a4e5f1 (diff) | |
Tentative amelioration pretty-printing symboles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4402 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files 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 *) () |