From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 25 Jan 2001 15:06:33 +0000 (+0000)
Subject: ex_ind treated similarly to exT_ind.
X-Git-Tag: no-uwobo~8
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=579125fc2d6b5573f287c6901c8c4f7265a1e2e5;p=helm.git

ex_ind treated similarly to exT_ind.
---

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')