added notations for abstact polinomials

HTML rendering of constants in symbol font improved (including m:minus)
added a title for the HTML rendering window

diff --git a/helm/style/arith.xsl b/helm/style/arith.xsl
index aabee3575c527ba4f665664bd142a5925ef48960..c9f3a2a1e4f684538484108bce7f0537c31c0af5 100644 (file)
--- a/helm/style/arith.xsl
+++ b/helm/style/arith.xsl
@@ -37,56 +37,64 @@
 <!-- ************************** ARITHMETICS ****************************** -->
 
 <xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Peano/le.ind']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="MUTIND"/>
       <xsl:with-param name="m-tag" select="'leq'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/lt.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'lt'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/ge.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'geq'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/gt.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'gt'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/plus.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'plus'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Arith/Minus/minus.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'minus'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/mult.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'times'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Arith/Min/min.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'min'"/>
    </xsl:call-template>

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 5aafef63f6bfb347b801b74fd3d35dbe2acb0916..f736dbd22ed431c447afd7863695c1735bf7cebc 100644 (file)
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -158,12 +158,16 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 </xsl:template>
 
 <xsl:template match="CONST" mode="pure">
-    <m:ci definitionURL="{@uri}" helm:xref="{@id}">
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri">
-      <xsl:with-param name="uri" select="@uri"/>
-     </xsl:call-template></xsl:with-param></xsl:call-template>
-     <!-- <xsl:value-of select="document(concat(string($absPath),@uri))/*/@name"/> -->
-    </m:ci>
+   <m:ci definitionURL="{@uri}" helm:xref="{@id}">
+      <xsl:call-template name="insert_subscript">
+         <xsl:with-param name="node_value">
+            <xsl:call-template name="name_of_uri">
+               <xsl:with-param name="uri" select="@uri"/>
+            </xsl:call-template>
+         </xsl:with-param>
+      </xsl:call-template>
+ <!-- <xsl:value-of select="document(concat(string($absPath),@uri))/*/@name"/> -->
+   </m:ci>
 </xsl:template>
 
 <xsl:template match="MUTIND" mode="pure">

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 028f65504cfa970ec95bd0e6dfa5f299ad62c784..b5706d60c29f91a00ce635b5922379261e22c546 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -29,9 +29,11 @@
 
 <!--***********************************************************************--> 
 <!-- From MathML content to HTML                                           -->
-<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi               -->
 <!--***********************************************************************--> 
 
+<xsl:param name="CICURI" select="''"/>
+
 <xsl:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
 <xsl:include href="html_reals.xsl"/>
@@ -58,19 +60,18 @@
 <xsl:variable name="framewidth" select="45"/>
 
 <xsl:template match="/">
- <xsl:param name="current_indent" select="0"/>
-               <html> 
-                <head>
-                 <style>
-                 A { text-decoration: none }
-                 </style>
-                </head>
-                <body bgcolor="white">
-                <xsl:apply-templates>
-                 <xsl:with-param name="current_indent" select="0"/>
-                </xsl:apply-templates>
-                </body>
-               </html>
+   <xsl:param name="current_indent" select="0"/>
+   <html> 
+      <head>
+        <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
+         <style> A { text-decoration: none } </style>
+      </head>
+      <body bgcolor="white">
+         <xsl:apply-templates>
+            <xsl:with-param name="current_indent" select="0"/>
+         </xsl:apply-templates>
+      </body>
+   </html>
 </xsl:template>
 
 <!--***********************************************************************-->
@@ -158,7 +159,7 @@
     <xsl:when test="$name='arrow'">
      <xsl:text>(</xsl:text>
      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <FONT color="blue" FACE="symbol">
+     <FONT color="blue" SIZE="+2" FACE="symbol">
       <xsl:text>&#x00ae;</xsl:text>
      </FONT>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
@@ -284,6 +285,14 @@
      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
      <xsl:apply-templates mode="inline" select="*[7]"/>
     </xsl:when>
+   
+      <!-- INTERP -->
+      <xsl:when test="$name='interp'">
+         <font color="green">[</font>
+            <xsl:apply-templates select="*[2]"/>
+         <font color="green">]</font>
+      </xsl:when>
+
    </xsl:choose>
 </xsl:template>
 
@@ -375,7 +384,7 @@
         <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
        </xsl:call-template>
        <!-- -> -->
-       <FONT color="blue" FACE="symbol">
+       <FONT color="blue" SIZE="+2" FACE="symbol">
         <xsl:text>&#x00ae;</xsl:text>
        </FONT>
        <xsl:apply-templates select="*[position()=3]">
@@ -1018,6 +1027,14 @@
         <xsl:with-param name="current_indent" select="$current_indent"/>
        </xsl:apply-templates>
       </xsl:when>
+
+      <!-- INTERP -->
+      <xsl:when test="$name='interp'">
+         <font color="green">[</font>
+            <xsl:apply-templates select="*[2]"/>
+         <font color="green">]</font>
+      </xsl:when>
+
      </xsl:choose>
 </xsl:template>
 

diff --git a/helm/style/contentlib.xsl b/helm/style/contentlib.xsl
index 5fcc918a792ff691eb3cf6c24158652b3d82824d..6efe8d6c993476cca6bdbb24a660cf5f9424bda8 100644 (file)
--- a/helm/style/contentlib.xsl
+++ b/helm/style/contentlib.xsl
@@ -34,11 +34,12 @@
                               xmlns:helm="http://www.cs.unibo.it/helm"
                               xmlns:xlink="http://www.w3.org/1999/xlink">
 
-<xsl:template name="mk-mml-infix"> <!-- make MML node for infix operator --> 
-   <xsl:param name="c-tag"/>       <!-- CIC    tag -->
-   <xsl:param name="m-tag"/>       <!-- MathML tag -->
+<xsl:template name="mkmml-op-noannot"> <!-- make MML node for operators (noannot mode) --> 
+   <xsl:param name="arity"/>           <!-- operator arity        -->
+   <xsl:param name="c-tag"/>           <!-- CIC    tag            -->
+   <xsl:param name="m-tag"/>           <!-- MathML tag            -->
    <xsl:choose>
-      <xsl:when test="count(child::*) = 3">
+      <xsl:when test="count(child::*) = $arity + 1">
          <m:apply helm:xref="{@id}">
             <xsl:element name="{concat('m:',$m-tag)}">
                <xsl:attribute name="definitionURL">
@@ -48,8 +49,45 @@
                   <xsl:value-of select="$c-tag/@id"/>
                </xsl:attribute>
             </xsl:element>
-            <xsl:apply-templates select="*[2]" mode="noannot"/>
-            <xsl:apply-templates select="*[3]" mode="noannot"/>
+            <xsl:apply-templates select="*[position() > 1]" mode="noannot"/>
+         </m:apply>
+      </xsl:when>
+      <xsl:otherwise>
+         <xsl:apply-imports/>
+      </xsl:otherwise>
+   </xsl:choose>
+</xsl:template>
+
+<xsl:template name="start-interp"> <!-- interp mode starter -->
+   <xsl:param name="rtree"/>
+   <xsl:param name="atree"/>   
+   <m:apply helm:xref="{@id}">
+      <m:csymbol>interp</m:csymbol>
+      <xsl:apply-templates mode="interp" select="$rtree">
+         <xsl:with-param name="atree" select="$atree"/>
+      </xsl:apply-templates>
+   </m:apply>
+</xsl:template>
+
+<xsl:template name="mkmml-op-interp"> <!-- make MML node for operators (interp mode) --> 
+   <xsl:param name="arity"/>          <!-- operator arity        -->
+   <xsl:param name="c-tag"/>          <!-- CIC    tag            -->
+   <xsl:param name="m-tag"/>          <!-- MathML tag            -->
+   <xsl:param name="atree"/>          <!-- abstract tree pointer -->
+   <xsl:choose>
+      <xsl:when test="count(child::*) = $arity + 1">
+         <m:apply helm:xref="{@id}">
+            <xsl:element name="{concat('m:',$m-tag)}">
+               <xsl:attribute name="definitionURL">
+                  <xsl:value-of select="$c-tag/@uri"/> 
+               </xsl:attribute>
+               <xsl:attribute name="helm:xref">
+                  <xsl:value-of select="$c-tag/@id"/>
+               </xsl:attribute>
+            </xsl:element>
+            <xsl:apply-templates select="*[position() > 1]" mode="interp">
+              <xsl:with-param name="atree" select="$atree"/>
+           </xsl:apply-templates>
          </m:apply>
       </xsl:when>
       <xsl:otherwise>

diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl
index d2e5b278ed33fbf733cc727c38e1dd3e22e56121..760010530a7b22c181319849b1b46900993dd015 100644 (file)
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -36,5 +36,6 @@
 <xsl:include href="arith.xsl"/>        <!-- FG -->
 <xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>
+<xsl:include href="ring.xsl"/>        <!-- FG -->
 
 </xsl:stylesheet>

diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 66ff1c030c50a1975236776930997467d7829ebf..f8930ed05cc1938169e9ef74d03a51a56c60c67a 100644 (file)
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -76,7 +76,7 @@
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
   <a href="{$uri}">
-   <FONT FACE="symbol" mathcolor="blue">
+   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
     <xsl:value-of select="$symbol"/>
    </FONT>
   </a>
@@ -93,7 +93,7 @@
   <xsl:choose>
    <xsl:when test="count(child::*)=2">
     <a href="{$uri}">
-    <xsl:text>-</xsl:text>
+    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates mode="inline" select="*[2]"/>
    </xsl:when>
@@ -101,7 +101,7 @@
     <xsl:text>(</xsl:text>
     <xsl:apply-templates mode="inline" select="*[2]"/>
     <a href="{$uri}">
-     <xsl:text>-</xsl:text>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates mode="inline" select="*[3]"/>
     <xsl:text>)</xsl:text>
@@ -116,7 +116,7 @@
    <xsl:value-of select="m:not/@definitionURL"/>
   </xsl:variable>
      <a href="{$uri}">
-     <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#216;</FONT>
      </a>
      <xsl:apply-templates mode="inline" select="*[2]"/>
  </xsl:template>
@@ -128,7 +128,7 @@
    <xsl:value-of select="m:exists/@definitionURL"/>
   </xsl:variable>
   <a href="{$uri}">
-   <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
+   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#36;</FONT>
   </a>
   <xsl:apply-templates select="m:bvar/m:ci"/>
   <xsl:text>:</xsl:text>
@@ -196,7 +196,7 @@
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
      <a href="{$uri}">
-     <FONT FACE="symbol" mathcolor="blue">
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
       <xsl:value-of select="$symbol"/>
      </FONT>
      </a>
@@ -222,7 +222,7 @@
   <xsl:choose>
    <xsl:when test="count(child::*)=2">
     <a href="{$uri}">
-    <xsl:text>-</xsl:text>
+    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
     </a>
     <xsl:apply-templates select="*[2]">
      <xsl:with-param name="current_indent" select="$current_indent + 1"/>
@@ -243,7 +243,7 @@
        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
       </xsl:call-template>
       <a href="{$uri}">
-      <xsl:text>-</xsl:text>
+      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#45;</FONT>
       </a>
       <xsl:apply-templates select="*[3]">
        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -267,7 +267,7 @@
    <xsl:value-of select="m:not/@definitionURL"/>
   </xsl:variable>
      <a href="{$uri}">
-     <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#216;</FONT>
      </a>
      <xsl:apply-templates select="*[2]"/>
  </xsl:template>
@@ -286,7 +286,7 @@
   <xsl:choose>
     <xsl:when test="$charlength > $framewidth">
      <a href="{$uri}">
-      <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
+      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#36;</FONT>
      </a>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>

diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 3bff65d2be918111d2bf44f7de7e8635d213a216..3eb8264653316a9334d5ce5c8e66d0746d768717 100644 (file)
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -44,7 +44,7 @@
   </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
+    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:choose>
@@ -122,7 +122,7 @@
   <xsl:text>(</xsl:text>
   <xsl:apply-templates mode="inline" select="*[2]"/>
   <a href="{$uri}">
-   <FONT FACE="symbol" mathcolor="blue">
+   <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
     <xsl:value-of select="$symbol"/>
    </FONT>
   </a>
@@ -178,7 +178,7 @@
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
      <a href="{$uri}">
-      <FONT FACE="symbol" mathcolor="blue">
+      <FONT FACE="symbol" SIZE="+2" mathcolor="blue">
        <xsl:value-of select="$symbol"/>
       </FONT>
      </a>
@@ -204,7 +204,7 @@
   </xsl:variable>-->
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
+    <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:variable name="charlength">

diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl
index 7f3deaa9251c0c7620c4609dbe4b758750de2435..5f111875a028c4b76a96f04a3f00b73222b7fb43 100644 (file)
--- a/helm/style/reals.xsl
+++ b/helm/style/reals.xsl
@@ -131,77 +131,88 @@
 <!-- Binary Operations and Relations -->
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rle.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'leq'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'lt'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'geq'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'gt'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'plus'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'minus'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'times'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rdiv.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'divide'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'min'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmax.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'max'"/>
    </xsl:call-template>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con']" mode="pure">
-   <xsl:call-template name="mk-mml-infix">
+   <xsl:call-template name="mkmml-op-noannot">
+      <xsl:with-param name="arity" select="2"/>
       <xsl:with-param name="c-tag" select="CONST"/>
       <xsl:with-param name="m-tag" select="'power'"/>
    </xsl:call-template>