X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=e0225d72ee32af20b01e00713ae6f65405986436;hb=3ce27112fe93ced5f67cc6af8fc63037eba3f322;hp=21031d002fc10fba43eb915623f054d45743ecd0;hpb=3f9cb46b5e167955e85b3d2544f1bed90f1a25b7;p=helm.git

diff --git a/matita/components/content_pres/cicNotationLexer.ml b/matita/components/content_pres/cicNotationLexer.ml
index 21031d002..e0225d72e 100644
--- a/matita/components/content_pres/cicNotationLexer.ml
+++ b/matita/components/content_pres/cicNotationLexer.ml
@@ -52,8 +52,6 @@ let regexp we_proved = "we" utf8_blank+ "proved"
 let regexp we_have = "we" utf8_blank+ "have"
 let regexp let_rec = "let" utf8_blank+ "rec" 
 let regexp let_corec = "let" utf8_blank+  "corec"
-let regexp nlet_rec = "nlet" utf8_blank+ "rec" 
-let regexp nlet_corec = "nlet" utf8_blank+  "corec"
 let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident_start = ident_letter 
@@ -307,8 +305,6 @@ and level2_ast_token =
   lexer
   | let_rec -> return lexbuf ("LETREC","")
   | let_corec -> return lexbuf ("LETCOREC","")
-  | nlet_rec -> return lexbuf ("NLETREC","")
-  | nlet_corec -> return lexbuf ("NLETCOREC","")
   | we_proved -> return lexbuf ("WEPROVED","")
   | we_have -> return lexbuf ("WEHAVE","")
   | utf8_blank+ -> ligatures_token level2_ast_token lexbuf