From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Dec 2000 17:12:15 +0000 (+0000)
Subject: Some optimizations using the "sort" attribute.
X-Git-Tag: nogzip~97
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92e006b92f453568bdbca000992f064079d86536;p=helm.git

Some optimizations using the "sort" attribute.
---

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 1d7945dc2..3b653ad15 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -22,13 +22,16 @@
 
 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
 
-<xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
-  <xsl:choose> 
-   <xsl:when test="@id">
+<xsl:template match="PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
+<xsl:apply-templates select="." mode="pure"/>
+</xsl:template>
+
+<xsl:template match="LAMBDA|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
     <xsl:variable name="id" select="@id"/>
     <xsl:choose>
      <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
-     <xsl:when test="//InnerTypes/TYPE[@of=$id]">
+     <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
+     <xsl:when test="@sort='Prop'">
      <xsl:choose>
       <xsl:when test="name()= 'APPLY' and CONST[
  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
@@ -95,11 +98,6 @@
       <xsl:apply-templates select="." mode="pure"/>
      </xsl:otherwise>
     </xsl:choose>
-   </xsl:when>
-   <xsl:otherwise>
-    <xsl:apply-templates select="." mode="pure"/>
-   </xsl:otherwise>
-  </xsl:choose>
 </xsl:template>
 
 <xsl:template match="*" mode="copy-of-no-prop">