From 138e51f3dc9bd6a42b84e45f9bf2c681cd411393 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 23 Jan 2001 12:59:57 +0000
Subject: [PATCH] - Bug due to overloading of csymbol letin fixed. Now we have
 both let_in (for CIC LETIN) and letin (generated by proof transformation).

- Bug of apply_ind fixed. If the proof of A->B->C is not of
the form \x.\y.M, than no special treatment is done.
---
 helm/style/content.xsl      |  2 +-
 helm/style/mmlextension.xsl |  2 +-
 helm/style/proofs.xsl       | 12 +++++++++---
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index a8d2ae856..65f982512 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -81,7 +81,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <xsl:template match="LETIN" mode="pure">
     <m:apply helm:xref="{@id}">
-     <m:csymbol>letin</m:csymbol>
+     <m:csymbol>let_in</m:csymbol>
      <m:bvar>
       <m:ci>
        <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="letintarget/@binder"/></xsl:with-param></xsl:call-template>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 0d23a1837..24c4bdbe5 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -420,7 +420,7 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
-      <xsl:when test="$name='letin'">
+      <xsl:when test="$name='let_in'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
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)">
-- 
2.39.2