Porting to the new DTD for MoWGLI.

diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile
index 7bb47374da06bfadd423724e94ba9b4bfb111ec0..847efdb319e8b8ebfa80d496141238852bef4611 100644 (file)
--- 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 119effa3da0aef63c21d8aa58bbb76700e55211e..fbff431ccdd6ce8ed84a2f31fd46b7a130452fc5 100644 (file)
--- 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 17fc523cdd3b1c40aa5836f2d10874a5a36685b4..b37f5c255e0432a294e49da91f8c1d80176a1ee6 100644 (file)
--- 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 8b4c24520076e0c2454c91f2513b519cd3cf3a90..5eaefa3a8661637f08feffc68d06ed72edf34555 100644 (file)
--- 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 005821e6fbacddc8fa81007c67e1dd2004740f5a..10af6394aea5b234a578603b234f47838dcda39e 100644 (file)
--- 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 f52b64702e89623bc081fc68697aa1e587df5961..6a99d12ffa7b30c5fd2c84c1e8f0de634300220d 100644 (file)
--- 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 9384b8430537108af8476045f9dc4abfba5da0d7..5b2ca768fb7b3d8f90ba8c53fb5e383d420f5508 100644 (file)
--- 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">