From ce0467a0ad80e0b1558c9846d582d7f1c1df5a86 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 16:09:08 +0000 Subject: [PATCH] Bug fixed: a symbol must be formed of just one (unicode) character. --- helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 6bdbd8057..b28d3cae6 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -49,7 +49,7 @@ let regexp commentend = "**)" let regexp blanks = blank+ let regexp num = digit+ let regexp tex_token = '\\' alpha+ -let regexp symbol = symbol_char+ +let regexp symbol = symbol_char let regexp ident_cont = alpha | num | '_' | '\'' let regexp ident_cont' = ident_cont | tex_token let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) -- 2.39.2