From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Aug 2001 15:16:25 +0000 (+0000)
Subject: Proof explosion improved (= avoided) for:
X-Git-Tag: v0_1_3~89
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0da07547d92d5bcb9f9eac2399ccb6b700b9d03;p=helm.git

Proof explosion improved (= avoided) for:
 1) Proofs after lambda-introductions (linear proofs)
 2) Proofs after a rewriting step (linear proofs)
 3) Proofs after a letin1 (linear proofs)
---

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 75c8a745b..d0c8555b3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -988,8 +988,12 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- PROOF -->
       <xsl:when test="$name='proof'">
        <m:maction actiontype="toggle">
-        <!-- CSC: next if until the annotationHelper can handle mactions -->
-        <xsl:if test="not($explodeall)">
+        <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
+        <xsl:variable name="test" select="(not($explodeall)) and
+	   (not(preceding-sibling::*[1]/text()='letin1')) and
+	   (not(preceding-sibling::*[1]/text()='rw_step')) and
+	   (not(name(..)='m:lambda'))"/>
+        <xsl:if test="$test">
          <!-- Details hided (default) -->
          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
           <m:mtr>
@@ -1026,7 +1030,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mphantom>
               <m:mtext>_</m:mtext>
              </m:mphantom>
-             <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
             </m:mrow>
            </m:mrow>
           </m:mtd>