Some optimizations using the "sort" attribute.

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 1d7945dc26208c0d44c01cf991ad84d92a8b1882..3b653ad15aa38b1f64713976d8a901a61c4fec59 100644 (file)
--- 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">