From ce98548577a44fafd17f1d9ce42bca1e6db104fc Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Jul 2008 13:28:34 +0000
Subject: [PATCH] Bugs fixed: \frac is an infix operator \infrule is a prefix
 operator

---
 helm/software/components/content_pres/cicNotationParser.ml | 4 ++--
 helm/software/matita/help/C/sec_usernotation.xml           | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index d7da2ff82..21720c01d 100644
--- 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 1076338e6..66952a814 100644
--- 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>
-- 
2.39.2