X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=00696cc00d2cec8b36e4a3a4a1c8d45000331a52;hb=190c0efe22d097c4b4e85207342224622b1fccb9;hp=bbf7de133addba6e2e2cb93a60d6ffda753f56ba;hpb=fd93fa0155994b70482e0f07d8e45c238cce835d;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index bbf7de133..00696cc00 100644
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -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*