]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.ml
typo s/\\OF/\\of/
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml
index 85b89451118d4cdf8cf923a4f9b2fbe7b242e916..7c52560bec68b7517a52ff5db2d9e55cc13822bf 100644 (file)
@@ -340,7 +340,7 @@ EXTEND
       | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
           return_term loc (Layout (Frac (p1, p2)))
       | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Layout (Sqrt p))
-      | SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
+      | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
           return_term loc (Layout (Root (arg, index)))
       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
           return_term loc (Layout (Box ((H, false, false), p)))