diff options
| author | herbelin | 2006-01-14 10:04:53 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-14 10:04:53 +0000 |
| commit | 5a7b0415facbaa1b44ee7c86a3b56aabe2ea40ab (patch) | |
| tree | 23ca97f1102c3091390e0d1464d3639456484708 /parsing | |
| parent | c9e1c00b4995d93c8fd3bb7e56c51907e6c668c6 (diff) | |
Code mort du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index c241ca2842..caae659ec3 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -381,11 +381,6 @@ let rec next_token = parser bp | TokIdent id -> (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)) - (* iso 8859-1 accentuated letters *) - | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c) ; - t = process_chars bp c >] -> - comment_stop bp; - t | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; (("INT", get_buff len), (bp, ep)) |