From: Pietro Di Lena <pietro.dilena@unibo.it>
Date: Thu, 21 Nov 2002 17:14:32 +0000 (+0000)
Subject: Porting to the new DTD for MoWGLI.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adbb8f993af86259003d7978a26de549b3aef2ae;p=helm.git

Porting to the new DTD for MoWGLI.
---

diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile
index 7bb47374d..847efdb31 100644
--- a/helm/meta_style/Makefile
+++ b/helm/meta_style/Makefile
@@ -1,7 +1,7 @@
 XSLTPROC = xsltproc --timing
 FORMAT = xmllint --format
 SUBST = ./subst.pl
-METASTYLESHEET = meta_cic2mathml.xsl
+METASTYLESHEET = ./meta_cic2mathml.xsl
 TMP1 = .tmpfile1
 TMP2 = .tmpfile2
 
diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml
index 119effa3d..fbff431cc 100644
--- a/helm/meta_style/algebra.xml
+++ b/helm/meta_style/algebra.xml
@@ -6,28 +6,28 @@
 
 <Operator
  name  = "0"
- uri   = "cic:/Algebra/CSemiGroups/csg_unit.con"
+ uri   = "cic:/Algebra/algebra/CSemiGroups/csg_unit.con"
  arity = "1">
 	<mop tag="ci" helm:xref="$APP-ID">0</mop>
 </Operator>
 
 <Operator
  name  = "1"
- uri   = "cic:/Algebra/CRings/cr_one.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_one.con"
  arity = "1">
 	<mop tag="ci" helm:xref="$APP-ID">1</mop>
 </Operator>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CGroups/cg_inv.con"
+ uri   = "cic:/Algebra/algebra/CGroups/cg_inv.con"
  hide  = "1"
  arity = "1"
  m-tag = "minus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con"
+ uri   = "cic:/Algebra/reals/CMetricFields/cmf_abs.con"
  hide  = "1"
  arity = "2"
  m-tag = "abs"/>
@@ -36,63 +36,63 @@
 
 <Operator
  name  = "SETOID EQUALITY"
- uri   = "cic:/Algebra/CSetoids/cs_eq.con"
+ uri   = "cic:/Algebra/algebra/CSetoids/cs_eq.con"
  hide  = "1"
  arity = "2"
  m-tag = "eq"/>
 
 <Operator
  name  = "APART"
- uri   = "cic:/Algebra/CSetoids/cs_ap.con"
+ uri   = "cic:/Algebra/algebra/CSetoids/cs_ap.con"
  hide  = "1"
  arity = "2"
  m-tag = "neq"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/leEq.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/leEq.con"
  hide  = "1"
  arity = "2"
  m-tag = "leq"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/cof_less.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/cof_less.con"
  hide  = "1"
  arity = "2"
  m-tag = "lt"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_plus.con | cic:/Algebra/CSemiGroups/csg_op.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_plus.con | cic:/Algebra/algebra/CSemiGroups/csg_op.con"
  hide  = "1"
  arity = "2"
  m-tag = "plus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_minus.con | cic:/Algebra/CGroups/cg_minus.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_minus.con | cic:/Algebra/algebra/CGroups/cg_minus.con"
  hide  = "1"
  arity = "2"
  m-tag = "minus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_mult.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_mult.con"
  hide  = "1"
  arity = "2"
  m-tag = "times"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CFields/cf_div.con"
+ uri   = "cic:/Algebra/algebra/CFields/cf_div.con"
  hide  = "1"
  arity = "2"
  m-tag = "divide"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/Ring_constructions/nzpro.con"
+ uri   = "cic:/Algebra/algebra/CRings/nzpro.con"
  cook  = "true"
  arity = "2">
 	<param id="1"/>
@@ -100,14 +100,14 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/exponentiation/nexp.con"
+ uri   = "cic:/Algebra/algebra/CRings/nexp.con"
  cook  = "true"
  arity = "2"
  m-tag = "power"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/exponentiation/nexp_op.con | cic:/Algebra/Expon/Zexp_def/zexp.con"
+ uri   = "cic:/Algebra/algebra/CRings/nexp_op.con | cic:/Algebra/algebra/Expon/zexp.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -120,7 +120,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/absSmall.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/absSmall.con"
  hide  = "1"
  arity = "2">
 	<mapp>
@@ -135,7 +135,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con"
+ uri   = "cic:/Algebra/algebra/CPolynomials/cpoly_apply_fun.con"
  cook  = "true"
  arity = "2"> 
  	<mapp>
@@ -147,7 +147,7 @@
 
 <Operator
  name  = "********"
- uri   = "cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/seqLimit.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -166,7 +166,7 @@
 
 <Operator
  name  = "********"
- uri   = "cic:/Algebra/CSums/Sums/sum0.con"
+ uri   = "cic:/Algebra/algebra/CSums/sum0.con"
  cook  = "true"
  arity = "2">
 	<m:apply helm:xref="$OP-ID">
@@ -185,7 +185,7 @@
 
 <Operator
  name  = "SUM"
- uri   = "cic:/Algebra/CSums/Sums/sum.con"
+ uri   = "cic:/Algebra/algebra/CSums/sum_.con"
  cook  = "true"
  arity = "3">
 	<m:apply helm:xref="$OP-ID">
diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml
index 17fc523cd..b37f5c255 100644
--- a/helm/meta_style/arith.xml
+++ b/helm/meta_style/arith.xml
@@ -32,7 +32,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zplus.con"
+ uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/Zplus.con"
  arity = "2"
  m-tag = "plus"/>
 
@@ -44,7 +44,7 @@
  
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zmult.con"
+ uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/Zmult.con"
  arity = "2"
  m-tag = "times"/>
 
@@ -56,7 +56,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/ZArith/fast_integer/fast_integers/Zopp.con"
+ uri   = "cic:/Coq/ZArith/fast_integer/Zopp.con"
  arity = "1"
  m-tag = "minus"/>
 
diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml
index 8b4c24520..5eaefa3a8 100644
--- a/helm/meta_style/basic.xml
+++ b/helm/meta_style/basic.xml
@@ -7,13 +7,13 @@
 
 <Operator
  name  = "AND"
- uri   = "cic:/Coq/Init/Logic/Conjunction/and.ind"
+ uri   = "cic:/Coq/Init/Logic/and.ind"
  arity = "2"
  m-tag = "and"/>
 
 <Operator
  name  = "OR"
- uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
+ uri   = "cic:/Coq/Init/Logic/or.ind"
  arity = "2"
  m-tag = "or"/>
 
@@ -28,14 +28,14 @@
 
 <Operator
  name  = "EQUALITY and TYPE EQUALITY"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2"
  m-tag = "eq"/>
 
 <NotOperator
  name  = "NOT-EQ and NOT-EQT"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2">
 	<mapp>
@@ -47,7 +47,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
+ uri   = "cic:/Coq/Init/Logic/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
  arity = "2">
 	<mapp>
 		<mop tag="exist"/>
@@ -61,7 +61,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
+ uri   = "cic:/Coq/Init/Logic/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
  hide  = "1"
  arity = "2">
 	<mapp>
diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl
index 005821e6f..10af6394a 100644
--- a/helm/meta_style/meta_cic2mathml.xsl
+++ b/helm/meta_style/meta_cic2mathml.xsl
@@ -47,6 +47,7 @@
 	<oxsl:include href="{@href}"/>
 </xsl:template>
 
+
 <xsl:template match="Operator|NotOperator">
 	<xsl:variable name="uri">
 		<xsl:call-template name="remove_white_spaces">
@@ -80,7 +81,7 @@
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
 			</xsl:variable>
-			
+
 			<!-- All uris in uri2 list (if not empty) have MUTIND c-tag -->
 			<xsl:variable name="uri2">
 				<xsl:call-template name="select_uris">
@@ -94,12 +95,23 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="arity" select="@arity"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="arity" select="@arity"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -107,12 +119,23 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="arity" select="@arity"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'MUTIND'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="arity" select="@arity"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -163,11 +186,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -175,11 +208,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'MUTIND'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -199,11 +242,7 @@
 	<xsl:param name="arity" select="0"/>
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
-
-	<xsl:variable name="apply_not">
-		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
-	</xsl:variable>
-
+	
 	<xsl:variable name="match">
 		<xsl:call-template name="out_match">
 			<xsl:with-param name="not"   select="$not"/>
@@ -215,61 +254,20 @@
 		</xsl:call-template>	
 	</xsl:variable>
 
-	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
-				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="c-tag" select="$c-tag"/>
-				<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
-			</xsl:call-template>
-		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
-	</xsl:variable>
-
 	<!--                     TEMPLATE                     -->
 	<xsl:call-template name="out_comment">
 		<xsl:with-param name="name" select="$name"/>
 	</xsl:call-template>
 
 	<oxsl:template match="{$match}" mode="pure">
-		<xsl:choose>
-			<xsl:when test="$cook = 'true'">
-				<oxsl:variable name="no_params">
-					<oxsl:variable name="no_params_tmp">
-						<oxsl:call-template name="get_no_params">
-							<oxsl:with-param name="first_uri"  select="$CICURI"/>
-							<oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-						</oxsl:call-template>
-					</oxsl:variable>
-					<oxsl:value-of select="number($no_params_tmp)"/>
-				</oxsl:variable>
-				<oxsl:choose>
-					<oxsl:when test="{concat('count(',$apply_not,'*) = $no_params + ',$arity + $hide + 1)}">
-						<xsl:call-template name="out_body">
-							<xsl:with-param name="c-tag" select="$c-tag"/>
-							<xsl:with-param name="m-tag" select="$m-tag"/>
-							<xsl:with-param name="cook"  select="$cook"/>
-							<xsl:with-param name="hide"  select="$hide"/>
-							<xsl:with-param name="arity" select="$arity"/>
-							<xsl:with-param name="not"   select="$not"/>
-						</xsl:call-template>
-					 </oxsl:when>
-					 <oxsl:otherwise>
-					 	<oxsl:apply-imports/>
-					</oxsl:otherwise>
-				</oxsl:choose>
-			</xsl:when>
-			<xsl:otherwise>
-				<xsl:call-template name="out_body">
-					<xsl:with-param name="c-tag" select="$c-tag"/>
-					<xsl:with-param name="m-tag" select="$m-tag"/>
-					<xsl:with-param name="cook"  select="$cook"/>
-					<xsl:with-param name="hide"  select="$hide"/>
-					<xsl:with-param name="arity" select="$arity"/>
-					<xsl:with-param name="not"   select="$not"/>
-				</xsl:call-template>
-			</xsl:otherwise>
-		</xsl:choose>
+		<xsl:call-template name="out_body">
+			<xsl:with-param name="c-tag" select="$c-tag"/>
+			<xsl:with-param name="m-tag" select="$m-tag"/>
+			<xsl:with-param name="cook"  select="$cook"/>
+			<xsl:with-param name="hide"  select="$hide"/>
+			<xsl:with-param name="arity" select="$arity"/>
+			<xsl:with-param name="not"   select="$not"/>
+		</xsl:call-template>
 	</oxsl:template>
 </xsl:template>
 
@@ -282,13 +280,10 @@
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params + </xsl:if>
-	</xsl:variable>
-
 	<xsl:variable name="match">
 		<xsl:call-template name="out_match_op">
-			<xsl:with-param name="not"   select="$not"/> 
+			<xsl:with-param name="not"   select="$not"/>
+			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="uri"   select="$uri"/> 
 			<xsl:with-param name="c-tag" select="$c-tag"/>
 		</xsl:call-template>
@@ -299,13 +294,10 @@
 	</xsl:variable>
 
 	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
-				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="c-tag" select="$c-tag"/>
-			</xsl:call-template>
-		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
+		<xsl:call-template name="op_uri_attr">
+			<xsl:with-param name="not"   select="$not"/>
+			<xsl:with-param name="c-tag" select="$c-tag"/>
+		</xsl:call-template>
 	</xsl:variable>
 
 
@@ -315,20 +307,9 @@
 	</xsl:call-template>
 	
 	<oxsl:template match="{concat('APPLY[',$match,']')}" mode="pure">
-		<xsl:if test="$cook = 'true'">
-			<oxsl:variable name="no_params">
-				<oxsl:variable name="no_params_tmp">
-					<oxsl:call-template name="get_no_params">
-						<oxsl:with-param name="first_uri"  select="$CICURI"/>
-						<oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-					</oxsl:call-template>
-				</oxsl:variable>
-				<oxsl:value-of select="number($no_params_tmp)"/>
-			</oxsl:variable>
-		</xsl:if>	
 		<oxsl:choose>
 			<xsl:for-each select="Case">
-				<oxsl:when test="{concat('count(',$apply_not,'*) = ',$no_params_var,@arity + $hide + 1)}">
+				<oxsl:when test="{concat('count(',$apply_not,'*) = ',@arity + $hide + 1)}">
 					<xsl:call-template name="out_body">
 						<xsl:with-param name="c-tag" select="$c-tag"/>
 						<xsl:with-param name="m-tag" select="$m-tag"/>
@@ -359,7 +340,12 @@
 <xsl:template name="out_match_op">
 	<xsl:param name="not"  select="'false'"/>
 	<xsl:param name="uri"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
+
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 	
 	<!-- application with not operator -->
 	<xsl:variable name="app_not">
@@ -374,36 +360,26 @@
 
 	<xsl:variable name="app_op">
 		<xsl:if test="$not = 'true'">APPLY[</xsl:if>
-		<xsl:value-of select="concat($c-tag,'[',$uris,']')"/>
+		<xsl:value-of select="concat($instantiate,$c-tag,'[',$uris,']')"/>
 		<xsl:if test="$not = 'true'">]</xsl:if>
 	</xsl:variable>
 
 	<xsl:value-of select="concat($app_not,$app_op)"/>
 </xsl:template>
 
+
 <!-- Returns a test on apply node children number-->
 <xsl:template name="out_match_child">
 	<xsl:param name="not"   select="'false'"/>
-	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 	<xsl:param name="arity" select="0"/>
 
-	<!--
-		Test on children number only if the operator is concatenated with not of 
-		if it is not constant and it has not to be cooked.
-		It is not possible to concatenate a constant operator with not.
-	-->
-	<xsl:if test="$not = 'true' or (($arity != 0 or $hide != 0) and $cook = 'false')">
+	<!-- Test on children number only if the operator is not constant -->
+	<xsl:if test="$arity != 0 or $hide != 0">
 		<xsl:choose>
 			<!-- if the operator has been concatenated with not, the root apply node must have only two child -->
 			<xsl:when test="$not = 'true'">
-				<xsl:variable name="test_apply_children">
-					<xsl:if test="$cook = 'false'">
-						<xsl:value-of select="concat(' and count(*[2]/*) = ',$arity + $hide + 1)"/>
-					</xsl:if>
-				</xsl:variable>
-				
-				<xsl:value-of select="concat('count(*) = 2',$test_apply_children)"/>
+				<xsl:value-of select="concat('count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>	
 			</xsl:when>
 			<xsl:otherwise>
 				<xsl:value-of select="concat('count(*) = ',$arity + $hide + 1)"/>
@@ -425,6 +401,7 @@
 		<xsl:call-template name="out_match_op">
 			<xsl:with-param name="not"   select="$not"/>
 			<xsl:with-param name="uri"   select="$uri"/>
+			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 			<xsl:with-param name="c-tag" select="$c-tag"/>
 		</xsl:call-template>
@@ -434,7 +411,6 @@
 	<xsl:variable name="match_child">
 		<xsl:call-template name="out_match_child">
 			<xsl:with-param name="not"   select="$not"/>
-			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 			<xsl:with-param name="arity" select="$arity"/>
 		</xsl:call-template>
@@ -467,7 +443,6 @@
 
 <xsl:template name="out_params">
 	<xsl:param name="params" select="1"/>
-	<xsl:param name="cook"   select="'false'"/>
 	<xsl:param name="hide"   select="0"/>
 	<xsl:param name="not"    select="'false'"/>
 	<xsl:param name="mode"   select="'noannot'"/>
@@ -478,7 +453,6 @@
 			<xsl:call-template name="param">
 				<xsl:with-param name="id"    select="$params"/>
 				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="cook"  select="$cook"/>
 				<xsl:with-param name="hide"  select="$hide"/>
 			</xsl:call-template>
 		</xsl:variable>
@@ -487,7 +461,6 @@
 		
 		<xsl:call-template name="out_params">
 			<xsl:with-param name="params" select="$params + 1"/>
-			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="not"    select="$not"/>
 			<xsl:with-param name="mode"   select="$mode"/>
@@ -496,7 +469,6 @@
 	</xsl:if>
 </xsl:template>
 
-
 <xsl:template name="out_body">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -513,6 +485,7 @@
 			<xsl:variable name="definitionURL">
 				<xsl:call-template name="op_uri_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
 				</xsl:call-template>
@@ -521,6 +494,7 @@
 			 <xsl:variable name="helm:xref">
 			 	<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
 				</xsl:call-template>
@@ -539,8 +513,7 @@
 				</xsl:element>
 				<!--            PARAMS            -->
 				<xsl:call-template name="out_params">
-					<xsl:with-param name="cook"   select="$cook"/>
-					<xsl:with-param name="hide"   select="$hide"/>	
+					<xsl:with-param name="hide"   select="$hide"/>					
 					<xsl:with-param name="not"    select="$not"/>
 					<xsl:with-param name="arity"  select="$arity"/>
 				</xsl:call-template>
@@ -559,6 +532,7 @@
 	</xsl:choose>
 </xsl:template>
 
+
 <xsl:template name="out_mvar">
 	<xsl:param name="vname"/>
 	
@@ -578,7 +552,6 @@
 <xsl:template name="out_choose_binder">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	<xsl:param name="binder"/>
 	
@@ -588,7 +561,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 					<xsl:with-param name="not"           select="$not"/>
-					<xsl:with-param name="cook"          select="$cook"/>
 					<xsl:with-param name="hide"          select="$hide"/>
 					<xsl:with-param name="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -596,7 +568,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 					<xsl:with-param name="not"           select="$not"/>
-					<xsl:with-param name="cook"          select="$cook"/>
 					<xsl:with-param name="hide"          select="$hide"/>
 					<xsl:with-param name="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -606,7 +577,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -619,6 +589,7 @@
 	</xsl:if>
 </xsl:template>
 
+
 <!-- *********************************************************************** -->
 <!--                     META LANGUAGE FOR MathML                            --> 
 <!-- *********************************************************************** -->
@@ -636,6 +607,7 @@
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
 					<xsl:with-param name="not"   select="$not"/>
@@ -647,6 +619,7 @@
 
 	<m:apply helm:xref="{$helm:xref}">
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="c-tag"  select="$c-tag"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="arity"  select="$arity"/>
@@ -664,7 +637,6 @@
 	</m:apply>
 </xsl:template>
 
-
 <xsl:template match="mop">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -678,6 +650,7 @@
 			<xsl:when test="@definitionURL">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@definitionURL"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -687,6 +660,7 @@
 			<xsl:otherwise>
 				<xsl:call-template name="op_uri_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
 				</xsl:call-template>
@@ -700,6 +674,7 @@
 			<xsl:when test="@xref">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -709,6 +684,7 @@
 			<xsl:otherwise>
 				<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$arity = 0 and $hide = 0"/>
 				</xsl:call-template>
@@ -725,6 +701,7 @@
 		</xsl:attribute>
 		
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="c-tag"  select="$c-tag"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="arity"  select="$arity"/>
@@ -742,8 +719,8 @@
 	</xsl:element>
 </xsl:template>
 
+
 <xsl:template match="param">
-	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="hide" select="0"/>
 	<xsl:param name="not"  select="'false'"/>
 
@@ -751,7 +728,6 @@
 		<xsl:call-template name="param">
 			<xsl:with-param name="id"    select="@id"/>
 			<xsl:with-param name="not"   select="$not"/>
-			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
@@ -779,6 +755,7 @@
 	</xsl:choose>
 </xsl:template>
 
+
 <xsl:template match="m:*">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -788,6 +765,7 @@
 	
 	<xsl:copy>
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="c-tag" select="$c-tag"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 			<xsl:with-param name="arity" select="$arity"/>
@@ -804,6 +782,7 @@
 	</xsl:copy>
 </xsl:template>
 
+
 <xsl:template match="mbvar">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -822,12 +801,11 @@
 		<xsl:call-template name="test_on_lambda">
 			<xsl:with-param name="binded_params" select="$binded_params"/>
 			<xsl:with-param name="not"           select="$not"/>
-			<xsl:with-param name="cook"          select="$cook"/>
 			<xsl:with-param name="hide"          select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
 
-	<xsl:variable name="binder">/target/@binder</xsl:variable>
+	<xsl:variable name="binder">/decl/@binder</xsl:variable>
 
 	<xsl:choose>
 		<xsl:when test="$binded_params != ''">
@@ -844,11 +822,10 @@
 											<xsl:with-param name="binded_params" select="$binded_params"/>
 											<xsl:with-param name="not"           select="$not"/>
 											<xsl:with-param name="hide"          select="$hide"/>
-											<xsl:with-param name="cook"          select="$cook"/>
 											<xsl:with-param name="binder"        select="$binder"/>
 										</xsl:call-template>
 									</oxsl:choose>
-								</oxsl:variable>
+ 								</oxsl:variable>
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="$binder"/>
 								</oxsl:call-template>
@@ -859,11 +836,10 @@
 									<xsl:call-template name="param">
 										<xsl:with-param name="id"    select="$binded_params"/>
 										<xsl:with-param name="not"   select="$not"/>
-										<xsl:with-param name="cook"  select="$cook"/>
 										<xsl:with-param name="hide"  select="$hide"/>
 									</xsl:call-template>
-								</xsl:variable>
-							
+								</xsl:variable>								
+
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="{concat($param,$binder)}"/>
 								</oxsl:call-template>
@@ -907,6 +883,8 @@
 	</xsl:choose>
 </xsl:template>
 
+
+
 <xsl:template match="mvar">
 	<xsl:call-template name="out_mvar">
 		<xsl:with-param name="vname" select="@name"/>
@@ -914,7 +892,6 @@
 </xsl:template>
 
 
-
 <!-- *********************************************************************** -->
 <!--                          AUXILIARY FUNCTIONS                            -->
 <!-- *********************************************************************** -->
@@ -1034,7 +1011,6 @@
 <xsl:template name="test_on_lambda">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	
 	<xsl:if test="$binded_params != ''">
@@ -1044,7 +1020,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1053,7 +1028,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1065,7 +1039,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1170,29 +1143,26 @@
 <xsl:template name="param">
 	<xsl:param name="id"/>
 	<xsl:param name="not"   select="'false'"/>
-	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 
 	<xsl:variable name="apply_not">
 		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
 	</xsl:variable>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params+</xsl:if>
-	</xsl:variable>
-
-	<xsl:value-of select="concat($apply_not,'*[',$no_params_var,$id + $hide + 1,']')"/>
+	<xsl:value-of select="concat($apply_not,'*[',$id + $hide + 1,']')"/>
 </xsl:template>
 
 <!-- Returns a xpath string with the location of the operator uri attribute -->
 <xsl:template name="op_uri_attr">
 	<xsl:param name="not"   select="'false'"/>
+	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@uri'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1201,12 +1171,14 @@
 <!-- Returns a xpath string with the location of the operator id attribute -->
 <xsl:template name="op_id_attr">
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 	
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@id'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1217,8 +1189,13 @@
 <xsl:template name="op_attr">
 	<xsl:param name="attr_type"/>
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
+	
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 
 	<xsl:variable name="apply">
 		<xsl:if test="$not = 'true'">APPLY/</xsl:if>
@@ -1229,12 +1206,13 @@
 			<xsl:value-of select="concat('{',$attr_type,'}')"/>	
 		</xsl:when>
 		<xsl:otherwise>
-			<xsl:value-of select="concat('{',$apply,$c-tag,'/',$attr_type,'}')"/> 			
+			<xsl:value-of select="concat('{',$apply,$instantiate,$c-tag,'/',$attr_type,'}')"/> 			
 		</xsl:otherwise>
 	</xsl:choose>
 </xsl:template>
 
 <xsl:template name="copy_attributes">
+	<xsl:param name="cook"   select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="hide"   select="0"/>
 	<xsl:param name="arity"  select="0"/>
@@ -1252,6 +1230,7 @@
 			<xsl:attribute name="{name()}">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="."/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -1284,6 +1263,7 @@
 <xsl:template name="set_attribute">
 	<xsl:param name="attr"/>
 	<xsl:param name="c-tag"/>
+	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 	<xsl:param name="arity" select="0"/>
 	<xsl:param name="not"   select="'false'"/>
@@ -1297,10 +1277,11 @@
 					<xsl:otherwise>@uri</xsl:otherwise>
 				</xsl:choose>
 			</xsl:variable>
-
+			
 			<xsl:call-template name="op_attr">
 				<xsl:with-param name="attr_type" select="$attr_type"/>
 				<xsl:with-param name="not"       select="$not"/>
+				<xsl:with-param name="cook"      select="$cook"/>
 				<xsl:with-param name="c-tag"     select="$c-tag"/>
 				<xsl:with-param name="const"     select="$arity = 0 and $hide = 0"/>
 			</xsl:call-template>
diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl
index f52b64702..6a99d12ff 100644
--- a/helm/meta_style/positive.xsl
+++ b/helm/meta_style/positive.xsl
@@ -73,7 +73,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
 
 
 
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="0"/>
     <xsl:with-param name="exp" select="1"/>
@@ -81,7 +81,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </xsl:apply-templates>
 </xsl:template>
  
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
    <m:apply helm:xref="{@id}">
     <m:minus definitionURL="{*[1]/@uri}" helm:xref="{*[1]/@id}"/>
     <xsl:apply-templates select="*[2]" mode="Zpositive">
@@ -92,13 +92,13 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </m:apply>
 </xsl:template>
 
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='1']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='1']" mode="pure">
    <m:ci definitionURL="{@uri}" helm:xref="{@id}">0</m:ci>
 </xsl:template>
 
 <!-- prova di notazione per positive -->
 
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind']]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind']]" mode="pure">
    <xsl:apply-templates select="." mode="Zpositive">
     <xsl:with-param name="base" select="0"/>
     <xsl:with-param name="exp" select="1"/>
@@ -106,7 +106,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </xsl:apply-templates>
 </xsl:template>
 
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3']" mode="pure">
  <m:ci definitionURL="{@uri}" helm:xref="{@id}">1</m:ci>
 </xsl:template> 
 
@@ -116,7 +116,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
  <xsl:param name="iden" select="''"/>
  <xsl:choose>
   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='1']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='1']">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="$base + $exp"/>
     <xsl:with-param name="exp" select="2 * $exp"/>
@@ -124,14 +124,14 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr
    </xsl:apply-templates>
   </xsl:when>
   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT' 
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='2']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="$base"/>
     <xsl:with-param name="exp" select="2 * $exp"/>
     <xsl:with-param name="iden" select="$iden"/>
    </xsl:apply-templates>
   </xsl:when>
-  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3'">
+  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3'">
    <m:ci helm:xref="{$iden}"><xsl:value-of select="$base + $exp"/></m:ci>
   </xsl:when>
   <xsl:otherwise>
diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml
index 9384b8430..5b2ca768f 100644
--- a/helm/meta_style/set.xml
+++ b/helm/meta_style/set.xml
@@ -6,7 +6,7 @@
 
 <Operator
  name  = "IN"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri   = "cic:/Coq/Sets/Ensembles/In.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -18,7 +18,7 @@
 
 <NotOperator
  name  = "NOT IN"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri   = "cic:/Coq/Sets/Ensembles/In.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -30,85 +30,92 @@
 
 <Operator
  name  = "EMPTY SET"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook  = "true">
-	<mop tag="set" helm:xref="$APP-ID"/>
+ uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
+ cook  = "true"
+ arity = "1">
+		<mapp>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
+			<param id="1"/>
+			<mop tag="set" helm:xref="$APP-ID"/>
+		</mapp>
 </Operator>
 
 <Operator
  name  = "EMPTY SET"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook  = "true"
- arity = "1">
-	<mapp>
-		<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
-		<param id="1"/>
-		<mop tag="set" helm:xref="$APP-ID"/>
-	</mapp>
+ uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind">
+ 	<mop tag="set" helm:xref="$APP-ID"/>
 </Operator>
 
-<OpSet
- name  = "SINGLETON"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind"
- cook  = "true">
 
- 	<Case arity="1">
+<Operator
+ name  = "SINGLETON"
+ uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook  = "true"
+ arity = "1">
  		<mop tag="set" helm:xref="$APP-ID">
 			<param id="1"/>
 		</mop>
-	</Case>
+</Operator>
 
- 	<Case arity="2">
+<Operator
+ name  = "SINGLETON"
+ uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="2"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "COUPLE"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind"
- cook  = "true">
- 	
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook  = "true"
+ arity = "2">
 		<mop tag="set" helm:xref="$APP-ID">
 			<param id="1"/>
 			<param id="2"/>
 		</mop>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "COUPLE"
+ uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="3"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
 				<param id="2"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "TRIPLE"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind"
- cook  = "true">
- 
-	<Case arity="3">
+ uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook  = "true"
+ arity = "3">
 		<mop tag="set">
 			<param id="1"/>
 			<param id="2"/>
 			<param id="3"/>
 		</mop>
-	</Case>
+</Operator>
  
-	<Case arity="4">
+<Operator
+ name  = "TRIPLE"
+ uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook  = "true"
+ arity = "4">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="4"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
@@ -116,23 +123,25 @@
 				<param id="3"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "INTERSECTION"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="intersect"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>
 		</mapp>
-	</Case>
+</Operator>
 
- 	<Case arity="3">
+<Operator
+ name  = "INTERSECTION"
+ uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -142,23 +151,25 @@
 				<param id="2" mode="set"/>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "UNION"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Union.ind"
- cook  = "true">
-	
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="union"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>		
 		</mapp>
-	</Case>
+</Operator>
  
-	<Case arity="3">
+<Operator
+ name  = "UNION"
+ uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>	
@@ -168,12 +179,11 @@
 				<param id="2" mode="set"/>
 			</m:apply>	
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
 <Operator
  name  = "INCLUDED"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Included.con"
+ uri   = "cic:/Coq/Sets/Ensembles/Included.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -185,7 +195,7 @@
 
 <Operator
  name  = "STRICTLY INCLUDED"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con"
+ uri   = "cic:/Coq/Sets/Ensembles/Strict_Included.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -195,20 +205,23 @@
 	</mapp>
 </Operator>
 
-<OpSet
+<Operator
  name  = "SET-DIFF"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="setdiff"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "SET-DIFF"
+ uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>	
@@ -218,15 +231,13 @@
 				<param id="2" mode="set"/>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "ADD-ELEM"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Add.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="union"/>
 			<param id="1" mode="set"/>
@@ -234,9 +245,13 @@
 				<param id="2" mode="set"/>
 			</m:set>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "ADD-ELEM"
+ uri   = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -248,15 +263,13 @@
 				</m:set>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "SUBTRACT-ELEM"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="setdiff"/>
 			<param id="1" mode="set"/>
@@ -264,9 +277,13 @@
 				<param id="2"/>
 			</m:set>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "SUBTRACT-ELEM"
+ uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -278,12 +295,11 @@
 				</m:set>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
 <Operator
  name  = "CARD"
- uri   = "cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind"
+ uri   = "cic:/Coq/Sets/Finite_sets/cardinal.ind"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -298,7 +314,7 @@
 
 <Operator
  name  = "SIGMA"
- uri   = "cic:/Coq/Init/Specif/Subsets/sig.ind"
+ uri   = "cic:/Coq/Init/Specif/sig.ind"
  arity = "2">
 	<m:set>
 		<mbvar name="x">