ex_ind treated similarly to exT_ind.

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 6c3375d97c873b42d3ed4612f5677bbe9f5837ab..09045cef239c866d0b4ebba8c3b02ed2f1484e11 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -125,9 +125,10 @@
       <xsl:apply-templates mode="pure" select="*[6]"/>
      </m:apply>
     </xsl:when>
-    <!-- exT_ind -->
-    <xsl:when test="name()= 'APPLY' and CONST[
- attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] 
+    <!-- ex_ind, exT_ind -->
+    <xsl:when test="name()= 'APPLY' 
+ and (CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
+      CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])  
  and count(child::*) = 6 
  and name(*[5])='LAMBDA' 
  and name(*[5]/target/*[1])='LAMBDA'"> 
@@ -195,9 +196,9 @@
    </xsl:when>
 <!--**** Patch temporanea, per il problema dei threads ***-->
 <xsl:when test="(name()= 'APPLY' and 
- (CONST[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
-  or
-   CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'])
+ (CONST[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] or
+  CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
+  CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
  and count(child::*) = 6 
  and name(*[5])='LAMBDA' 
  and name(*[5]/target/*[1])='LAMBDA')