X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fproofs.xsl;h=081711c5311ab6b63c445dbe5537ef1982104ea5;hb=138e51f3dc9bd6a42b84e45f9bf2c681cd411393;hp=faf8d94ab0fd133b0674c76355c02bc6d62f5b5b;hpb=ec4278cb76dd6238be23a8883cd85f152d7c1ac7;p=helm.git

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index faf8d94ab..081711c53 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -97,10 +97,13 @@
       <xsl:apply-templates mode="thread" select="*[5]"/>
      </m:apply>
     </xsl:when>
-    <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
+    <!-- gestire meglio il caso di and_ind quando la prova 
+         non e' della forma \x.\y.M -->
     <xsl:when test="name()= 'APPLY' and CONST[
  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
- and count(child::*) = 6">
+ and count(child::*) = 6 
+ and name(*[5])='LAMBDA' 
+ and name(*[5]/target/*[1])='LAMBDA'"> 
      <m:apply helm:xref="{@id}">
       <m:csymbol>and_ind</m:csymbol>
       <xsl:apply-templates mode="noannot" select="*[6]"/>
@@ -176,7 +179,10 @@
 <!--**** Patch temporanea, per il problema dei threads ***-->
 <xsl:when test="(name()= 'APPLY' and CONST[
  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
- and count(child::*) = 6) or
+ and count(child::*) = 6 
+ and name(*[5])='LAMBDA' 
+ and name(*[5]/target/*[1])='LAMBDA')
+ or
 (name()= 'APPLY' and CONST[
  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
  and count(child::*) = 7)">