From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Dec 2002 11:43:18 +0000 (+0000)
Subject: Severe bug fixed: the test failed in the case of (Rplus (...) R1).
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94512047e60c9872c472081c193eae44bddefc65;p=helm.git

Severe bug fixed: the test failed in the case of (Rplus (...) R1).
As a consequence (Rplus (Rplus R1 R1) R1) was rendered as 2.
---

diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl
index baee6a907..e337b663e 100644
--- a/helm/meta_style/positive.xsl
+++ b/helm/meta_style/positive.xsl
@@ -193,7 +193,7 @@ and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']">
   </xsl:choose>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST[position() = 1 and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and CONST[position() = 2 and @uri='cic:/Coq/Reals/Rdefinitions/R1.con'] and count(*) = 3]" mode="reals">
+<xsl:template match="APPLY[*[position() = 1 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and *[position() = 2 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/R1.con'] and count(*) = 3]" mode="reals">
   <xsl:param name="real_counter" select="0"/>
   <xsl:variable name="result">
    <xsl:apply-templates select="*[3]" mode="reals">