Bugs fixed:

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

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index d7da2ff822d27f46a817820a11db23caf6ccd888..21720c01d5b40a3f41a9b3369fce8f335211b615 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -150,7 +150,7 @@ let extract_term_production pattern =
     | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
     | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
-    | Ast.InfRule (p1, p2, p3) -> aux p1 @ [NoBinding, gram_symbol "\\infrule"] @ aux p2 @ aux p3
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
     | Ast.Root (p1, p2) ->
@@ -425,7 +425,7 @@ EXTEND
       | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
-      | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
       | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->