- Bug due to overloading of csymbol letin fixed.

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

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index faf8d94ab0fd133b0674c76355c02bc6d62f5b5b..081711c5311ab6b63c445dbe5537ef1982104ea5 100644 (file)
--- 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)">