From 94512047e60c9872c472081c193eae44bddefc65 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Dec 2002 11:43:18 +0000
Subject: [PATCH] Severe bug fixed: the test failed in the case of (Rplus (...)
 R1). As a consequence (Rplus (Rplus R1 R1) R1) was rendered as 2.

---
 helm/meta_style/positive.xsl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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">
-- 
2.39.2