]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/arith.xsl
contentlib.xsl improved, now handles eq eqT
[helm.git] / helm / style / arith.xsl
index c9f3a2a1e4f684538484108bce7f0537c31c0af5..8b2ee122af006a26398e790640a8d9f8ce6b6c0e 100644 (file)
@@ -37,7 +37,7 @@
 <!-- ************************** ARITHMETICS ****************************** -->
 
 <xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Peano/le.ind']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -45,7 +45,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/lt.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -53,7 +53,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/ge.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -61,7 +61,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/gt.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -69,7 +69,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/plus.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -77,7 +77,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Arith/Minus/minus.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -85,7 +85,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Init/Peano/mult.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>
@@ -93,7 +93,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST/@uri='cic:/Coq/Arith/Min/min.con']" mode="pure">
-   <xsl:call-template name="mkmml-op-noannot">
+   <xsl:call-template name="mk-mml-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'"/>