- Procedural: generation of "exact" is now complete

[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index bbc901dab7db3e2f139e37e6e65639efe1d2abd4..ac3b1142252dda604e88ccde5c86b32af757865b 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -88,7 +88,8 @@ let level1_layouts =
   [ "sub"; "sup";
     "below"; "above";
     "over"; "atop"; "frac";
-    "sqrt"; "root"
+    "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
   ]
 
 let level1_keywords =
@@ -96,7 +97,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle" ; "mpadded"
+    "term"; "ident"; "number";
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -131,9 +132,7 @@ let _ =
   List.iter
     (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
-      ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
-      ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
-      ("==", <:unicode<equiv>>);
+      (":=", <:unicode<def>>);
     ]
 
 let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+