update in gruound

[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommLexer.mll

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
index 21cca9c6c21529ea6a4a3b0d5f7e1ad387496d53..83a2892472a11f3b2cfa72e937972cf995097175 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
@@ -5,18 +5,22 @@
 
   let keys = [|
     "Note";
+    "NOTE";
   |]
 
   let heads = [|
-    "Advanved";
+    "Advanced";
     "Basic";
     "Constructions";
     "Forward";
     "Destructions";
     "Eliminations";
     "Eliminators";
+    "Equalities";
+    "Helper";
     "Inversion";
     "Inversions";
+    "Iterators";
     "Main";
     "Properties";
   |]
@@ -34,9 +38,9 @@
     aux (String.length s - 1)
 
   let disambiguate_word s =
-    if is_uppercase_ascii s then EP.CW s else
     if Array.mem s keys then EP.KW s else
     if Array.mem s heads then EP.HW s else
+    if is_uppercase_ascii s then EP.CW s else
     EP.SW s
 
   let log s =
@@ -53,7 +57,7 @@ let CR = "\r"
 let SP = " "
 let NL = "\n"
 let SR = "*"
-let OP = "(*" SP*
+let OP = "(*"
 let CP = SR* "*)"  
 let PP = CP SP* OP
 let WF = ['A'-'Z' 'a'-'z']