Bugs fixed:

\frac is an infix operator
\infrule is a prefix operator

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 ->

diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 1076338e6e06050d6702f29f3acb360e6c9873f8..66952a8145e1bc0fb6d28ba11d4c8dc78c9267b1 100644 (file)
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -313,7 +313,7 @@
        <row>
         <entry></entry>
         <entry>|</entry>
-        <entry><emphasis role="bold">\frac</emphasis> &layout; &layout;</entry>
+        <entry>&layout; <emphasis role="bold">\frac</emphasis> &layout;</entry>
         <entry>Fraction</entry>
        </row>
        <row>