]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/set.xsl
Complete management of inductive types.
[helm.git] / helm / style / set.xsl
index 849365f3f6f155b1bda2ae33150525752dd6e99b..5ff4fce0b94642e447563375f7cf38dbb0d9dabf 100644 (file)
@@ -68,7 +68,7 @@
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -94,7 +94,7 @@
 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -118,7 +118,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -146,7 +146,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -176,7 +176,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -208,7 +208,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -242,7 +242,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -277,7 +277,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -311,7 +311,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -334,7 +334,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -357,7 +357,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -391,7 +391,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -429,7 +429,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="CONST/@uri"/>
      </xsl:call-template>
     </xsl:variable>
@@ -467,7 +467,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble
 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
-      <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
+      <xsl:with-param name="first_uri" select="$CICURI"/>
       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
      </xsl:call-template>
     </xsl:variable>