]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationLexer.ml
metavariable context has a separator now
[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml
index bbf7de133addba6e2e2cb93a60d6ffda753f56ba..00696cc00d2cec8b36e4a3a4a1c8d45000331a52 100644 (file)
@@ -50,10 +50,10 @@ let is_ligature_char =
       true
     with Not_found -> false))
 
-let regexp we_proved = "we" ' '+ "proved"
-let regexp we_have = "we" ' '+ "have"
-let regexp let_rec = "let" ' '+ "rec" 
-let regexp let_corec = "let" ' '+  "corec"
+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 ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident = ident_letter ident_cont* ident_decoration*