- <!-- NATIND 3 parametri -->
- <xsl:when test="name()='APPLY' and CONST[
- attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 4">
- <m:apply>
- <m:csymbol>nat_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
- </xsl:when>
- <!-- NATIND 4 parametri -->
- <xsl:when test="name()='APPLY' and CONST[
- attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] and count(child::*) = 5">
- <m:apply>
- <m:csymbol>nat_ind</m:csymbol>
- <xsl:apply-templates mode="noannot" select="*[3]"/>
- <xsl:apply-templates mode="noannot" select="*[4]"/>
- </m:apply>
+ <xsl:when test="CONST[1]">
+ <xsl:variable name="uri" select="CONST[1]/@uri"/>
+ <xsl:choose>
+ <xsl:when test="contains($uri,'_ind.con')">
+ <xsl:variable name="ind_uri"
+ select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+ <xsl:variable name="inductive_def"
+ select="document(concat(string($absPath),$ind_uri))/InductiveDefinition"/>
+ <!-- check if the corresponding inductive definition actually
+ exists -->
+ <xsl:choose>
+ <xsl:when test="$inductive_def">
+ <xsl:variable name="ind_name">
+ <xsl:call-template name="get_name">
+ <xsl:with-param name="uri" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="no_params">
+ <xsl:call-template name="get_no_params">
+ <xsl:with-param name="first_uri" select="$CICURI"/>
+ <xsl:with-param name="second_uri" select="$uri"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:apply-templates mode="inductive" select=".">
+ <xsl:with-param name="inductive_def_uri"
+ select="$ind_uri"/>
+ <xsl:with-param name="inductive_def"
+ select="$inductive_def"/>
+ <xsl:with-param name="section_params" select="$no_params"/>
+ <xsl:with-param name="inductive_def_index" select="1"/>
+ <xsl:with-param name="inductive_def_name" select="$ind_name"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="letin" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="letin" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>