xmlns:m="http://www.w3.org/1998/Math/MathML"
xmlns:helm="http://www.cs.unibo.it/helm">
-<!--xsl:import href="objcontent.xsl"/-->
+<xsl:import href="objcontent.xsl"/>
<xsl:include href="headercontent.xsl"/>
<xsl:include href="getter.xsl"/>
<!-- CIC DEFINITION -->
-<xsl:template match="Definition">
- <xsl:choose>
+<xsl:template match="ConstantType">
+ <xsl:choose>
<xsl:when test="$type='typeonly'">
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
</type>
</xsl:when>
<xsl:otherwise>
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<Params>
- <xsl:value-of select="@params"/>
+ <xsl:call-template name="var_name">
+ <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+ </xsl:call-template>
</Params>
</xsl:if>
- <body>
- <xsl:apply-templates select="body/*[1]"/>
- </body>
+ <body/>
<type>
- <xsl:apply-templates select="type/*[1]"/>
+ <xsl:apply-templates select="./*[1]" mode="noannot"/>
</type>
</Definition>
</xsl:otherwise>
- </xsl:choose>
+ </xsl:choose>
</xsl:template>
<xsl:template match="Axiom|CurrentProof|InductiveDefinition|Variable">
<xsl:apply-templates select="." mode="noannot"/>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
<m:math>
<xsl:apply-templates select="." mode="noannot"/>
</m:math>
</xsl:template>
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate" mode="noannot">
<xsl:apply-templates select="." mode="pure"/>
</xsl:template>
projects / helm.git / commitdiff