]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationLexer.ml
- hExtlib: added debugging information for split_nth
[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml
index ac3b1142252dda604e88ccde5c86b32af757865b..b13c7887f3b07acde439ce7854ce5a0627dc070c 100644 (file)
@@ -52,6 +52,8 @@ 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 = ident_letter ident_cont* ident_decoration*
@@ -284,6 +286,8 @@ 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