<xsl:template mode="inductive" match="APPLY">
- <xsl:param name="inductive_def_uri" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:param name="inductive_def" select="/.."/>
<xsl:param name="inductive_def_index" select="1"/>
<xsl:param name="inductive_def_name" select="''"/>
<xsl:param name="section_params" select="0"/>
<!-- expected_args_type contains the types of the arguments expected by
the induction principle -->
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
<xsl:variable name="expected_args_types"
- select="document(concat(string($absPath),*[1]/@uri))/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+ select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
<xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
<xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
<!-- First check that the induction principle is applied to the
<xsl:when test="string($argsOK) = 'true'">
<!-- arguments are in the expected form: we create a
"by_induction" content element -->
- <!-- inductive_def contains the inductive definition -->
- <xsl:variable name="inductive_def"
- select="document(concat(string($absPath),$inductive_def_uri))/InductiveDefinition"/>
<!-- no_params is the number of paramters in square brackets -->
<xsl:variable name="no_params"
select="$inductive_def/@noParams"/>
</xsl:choose>
</xsl:template>
-
</xsl:stylesheet>
-