diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-17 19:59:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-17 19:59:39 +0000 |
| commit | 2521bbc7e9805fd57d2852c1e9631250def11d57 (patch) | |
| tree | 6cdc089a8a07a033bc5089edb5bbaa3adb193412 /toplevel/metasyntax.ml | |
| parent | d25dfc1a30ab227178f8cd4304f28a35f4d7e19d (diff) | |
About "unsupported" unicode characters in notations.
- 8.2 (bug-fix): reverted check for unicode early at notation definition time
(an unsupported "cadratin" space, 0x2003, was used in CoRN!) [by the way,
what to do with unicode spacing characters in general?]
- trunk: improved error message, removed redundant code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 3d1981168..7564ee8ea 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -328,7 +328,6 @@ let rec raw_analyze_notation_tokens = function | String x :: sl when is_normal_token x -> NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> - Lexer.check_keyword s; Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl | WhiteSpace n :: sl -> Break n :: raw_analyze_notation_tokens sl |