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