aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2005-12-28 13:03:11 +0000
committerherbelin2005-12-28 13:03:11 +0000
commit800e5da47f16bf3294aae43556fe82db14a3301e (patch)
tree4ddc16a42150db036a1307ac188bbf2eb7ef20d7
parentfd70bb7da02f4f1b86dd850f57387bac9966ef12 (diff)
Commentaire mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7752 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/lexer.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 1708fa5eb5..c241ca2842 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -95,7 +95,6 @@ let check_ident str =
bad_token str
| _ ->
bad_token str)
- (* iso 8859-1 accentuated letters *)
| [< _ = Stream.empty >] -> ()
| [< >] -> bad_token str
in