From 107b7efc2281a24ab2a4ddd2cec88329f88ee8cb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Sep 2005 17:02:39 +0000 Subject: [PATCH] '!' is no longer a decorator (to allow a reasonable notation for factorial). --- helm/ocaml/cic_notation/cicNotationLexer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index db0eb3de8..c1701c96b 100644 --- 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* -- 2.39.2