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 baee6a907dc32489f78f1a09aa170b95b2b5de67..e337b663ee0d80ac1ddb00fce12d1b64b7175456 100644 (file)
--- 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">