'!' is no longer a decorator (to allow a reasonable notation for factorial).

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index db0eb3de8242e94c7f21d08afc78a0fc655a1783..c1701c96b821c92bcbbdef9147166e272f69235e 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -37,7 +37,7 @@ let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]
 let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ]
 let regexp ligature = ligature_char ligature_char+
 
-let regexp ident_decoration = '\'' | '!' | '?' | '`'
+let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident = ident_letter ident_cont* ident_decoration*