*** empty log message ***

[helm.git] / helm / style / proofs.xsl

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 96d1ee7de532142ee3ce9ac18f7e4c6644950351..c40a42ce865ac34e19b3b9af7daf04975fb72835 100644 (file)
--- 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')])"/>