From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 7 Mar 2001 08:40:27 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: v0_1_2~91
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ad14dd8ca7dde8d3a5a33ebc466d3ea77b4b6c6;p=helm.git

*** empty log message ***
---

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index cd17b6d4c..fffc45865 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -319,7 +319,7 @@
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
           <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
          </xsl:apply-templates>
          <br/>
          <xsl:call-template name="make_indent">
@@ -344,7 +344,7 @@
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
           <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
          </xsl:apply-templates><br/> 
          <xsl:call-template name="make_indent">
           <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
@@ -799,7 +799,7 @@
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">
         <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
        </xsl:apply-templates><br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
@@ -1003,10 +1003,10 @@ PROOF:
          <xsl:text>| </xsl:text>
          </xsl:otherwise>
          </xsl:choose>
-         <xsl:value-of select="./@name"/> 
+         <xsl:value-of select="./@name"/>
          <xsl:text>: </xsl:text>
          <xsl:apply-templates select="./*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+          <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
          </xsl:apply-templates>
       </xsl:for-each>
      </xsl:for-each>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 96d1ee7de..c40a42ce8 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -124,6 +124,7 @@
     </xsl:when>
     <!-- EQUALITY with extra-parameters -->
     <xsl:when test="name()= 'APPLY' and CONST[
+ attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
       <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>