From 579125fc2d6b5573f287c6901c8c4f7265a1e2e5 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 25 Jan 2001 15:06:33 +0000
Subject: [PATCH] ex_ind treated similarly to exT_ind.

---
 helm/style/proofs.xsl | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 6c3375d97..09045cef2 100644
--- 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')
-- 
2.39.2