- 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.

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index a8d2ae856004fb55d83d3324558f1d488632d09f..65f9825128b4eb13d0208c8b2def3e359ea71786 100644 (file)
--- 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 0d23a1837ce3803999615b9cc12d8571b9af275f..24c4bdbe50a2883e2ceaf2ea33f698f37bff29a8 100644 (file)
--- 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 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)">