]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: a symbol must be formed of just one (unicode) character.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 8 Jun 2005 16:09:08 +0000 (16:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 8 Jun 2005 16:09:08 +0000 (16:09 +0000)
helm/ocaml/cic_disambiguation/cicTextualLexer2.ml

index 6bdbd8057015a58cc7bd119ff38dc5fc463aa849..b28d3cae66de76a40b49725bdc829024dbcce848 100644 (file)
@@ -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+)