Notation for if then else.

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

diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl
index 0685f47b0da8f521378c7e260c558c27cceb8d59..0a261260a23154adcc6e268121f27d7abc7bde3f 100644 (file)
--- a/helm/style/logic.xsl
+++ b/helm/style/logic.xsl
@@ -47,7 +47,7 @@
 <xsl:template mode="proof_transform" match="APPLY[CONST[
  attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] and 
  count(child::*) = 6 and name(*[5])='LAMBDA' and 
- count(*[5]/decl) = 2]">
+ count(*[5]/decl) >= 2]">
   <xsl:variable name="id" select="@id"/>
   <m:apply helm:xref="{@id}">
    <m:csymbol>and_ind</m:csymbol>
@@ -56,7 +56,14 @@
    <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
    <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
    <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-   <xsl:apply-templates mode="noannot" select="*[5]/target/*"/> 
+   <xsl:choose>
+    <xsl:when test="count(*[5]/decl) = 2">
+     <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates select="*[5]/*[3]" mode="lambda_prop"/>
+    </xsl:otherwise>
+   </xsl:choose> 
   </m:apply>
 </xsl:template>
 
@@ -117,11 +124,12 @@
 -->
 </xsl:template> 
 
+
 <xsl:template mode="proof_transform" match="APPLY[CONST[
  attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
  attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
  count(child::*) = 6 and
- name(*[5])='LAMBDA' and count(*[5]/decl) = 2 ]">
+ name(*[5])='LAMBDA' and count(*[5]/decl) >= 2 ]">
   <xsl:variable name="id" select="@id"/>
    <m:apply helm:xref="{@id}">
     <m:csymbol>ex_ind</m:csymbol>
@@ -130,9 +138,18 @@
     <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
     <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-    <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+    <xsl:choose>
+     <xsl:when test="count(*[5]/decl) > 2">
+      <xsl:apply-templates mode="lambda_prop" select="*[5]/decl[3]"/>
+     </xsl:when>
+     <xsl:otherwise>     
+      <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+     </xsl:otherwise>
+    </xsl:choose>
    </m:apply>
 </xsl:template>
 
+
 </xsl:stylesheet>
 
+