]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/inductive.xsl
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / style / inductive.xsl
index f9b535f1e72e43a60299b80ed5da5494d51064ca..83569d751660cf0008629f29c8986d149b2f0441 100644 (file)
@@ -43,8 +43,9 @@
  <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:choose>
 </xsl:template>
 
-
 </xsl:stylesheet>
-