X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fset.xsl;h=f1f7b7e50b5bf56e470fa0592dec67b76b002d14;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=5ff4fce0b94642e447563375f7cf38dbb0d9dabf;hpb=d4b90e232867dd3cda85b7707ac456b547539a06;p=helm.git

diff --git a/helm/style/set.xsl b/helm/style/set.xsl
index 5ff4fce0b..f1f7b7e50 100644
--- a/helm/style/set.xsl
+++ b/helm/style/set.xsl
@@ -488,4 +488,51 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
     </xsl:choose>
 </xsl:template>
 
+<!-- *******************  SIGMA TYPES  **************************** -->
+
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/Subsets/sig.ind']]" mode="pure">
+ <xsl:choose>
+  <xsl:when test="count(child::*) = 3">
+   <xsl:choose>
+    <xsl:when test="name(*[3]) = 'LAMBDA'">
+     <m:set>
+       <m:bvar>
+        <m:ci>
+         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template>
+        </m:ci>
+        <m:type>
+         <xsl:apply-templates select="*[3]/source/*[1]" mode="noannot"/>
+        </m:type>
+       </m:bvar>
+       <m:condition>
+        <xsl:apply-templates select="*[3]/target/*[1]" mode="noannot"/>
+       </m:condition>
+     </m:set>
+    </xsl:when>
+    <xsl:otherwise>
+     <m:set>
+       <m:bvar>
+        <m:ci>$x</m:ci>
+        <m:type>
+         <xsl:apply-templates select="*[2]" mode="noannot"/>
+        </m:type>
+       </m:bvar>
+       <m:condition>
+        <m:apply>
+         <m:csymbol>app</m:csymbol>
+         <xsl:apply-templates select="*[3]" mode="noannot"/>
+         <m:ci>$x</m:ci>
+        </m:apply>
+       </m:condition>
+     </m:set>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-imports/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
 </xsl:stylesheet>