From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:09:08 +0000 (+0000)
Subject: Bug fixed: a symbol must be formed of just one (unicode) character.
X-Git-Tag: PRE_INDEX_1~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ce0467a0ad80e0b1558c9846d582d7f1c1df5a86;p=helm.git

Bug fixed: a symbol must be formed of just one (unicode) character.
---

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+)