From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Dec 2000 12:28:46 +0000 (+0000)
Subject: Update to V7 after V6-2 tag creationg
X-Git-Tag: nogzip~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd98b68b3d650913fc08e269ed03459d06648ca8;p=helm.git

Update to V7 after V6-2 tag creationg
---

diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl
index 148912aa1..449cd1c54 100644
--- a/helm/style/basic.xsl
+++ b/helm/style/basic.xsl
@@ -20,7 +20,7 @@
 
 <!-- AND -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Conjunction/and.ind'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Conjunction/and.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -30,7 +30,7 @@
 
 <!-- OR -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Disjunction/or.ind'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Disjunction/or.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:or definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -40,7 +40,7 @@
 
 <!-- NOT -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con'] and (count(child::*) = 2)]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con'] and (count(child::*) = 2)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:not definitionURL="{CONST/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -49,7 +49,7 @@
 
 <!-- IFF -->
 <!--
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/Equivalence/iff.ind'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/Equivalence/iff.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:iff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -60,7 +60,7 @@
 
 <!-- EXISTS -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/First_order_quantifiers/ex.ind' or attribute::uri='cic:/coq/INIT/Logic_Type/exT.ind'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind' or attribute::uri='cic:/Coq/Init/Logic_Type/exT.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
      <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:choose>
@@ -84,7 +84,7 @@
     </m:apply>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/First_order_quantifiers/ex2.ind' or attribute::uri='cic:/coq/INIT/Logic_Type/exT2.ind'] and (count(child::*) = 4)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind' or attribute::uri='cic:/Coq/Init/Logic_Type/exT2.ind'] and (count(child::*) = 4)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:exists definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:choose>
@@ -151,7 +151,7 @@
 
 <!-- EQUALITY -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Equality/eq.ind'] and (count(child::*) = 4)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Equality/eq.ind'] and (count(child::*) = 4)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[3]" mode="noannot"/>
@@ -162,7 +162,7 @@
 
 <!-- TYPE EQUALITY -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_Type/eqT.ind'] and (count(child::*) = 4)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_Type/eqT.ind'] and (count(child::*) = 4)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:eq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[3]" mode="noannot"/>
@@ -172,8 +172,8 @@
 
 <!-- NOT-EQ -->
 <!-- NOT and EQ have no parameters -->
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
-and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/Equality/eq.ind']]]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
+and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/Equality/eq.ind']]]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(APPLY/child::*) = 4">
       <m:apply helm:xref="{@id}">
@@ -189,8 +189,8 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic/E
 </xsl:template>
 
 <!-- NOT-EQT -->
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
-and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_Type/eqT.ind']]]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
+and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_Type/eqT.ind']]]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(APPLY/child::*) = 4">
       <m:apply helm:xref="{@id}">
@@ -212,7 +212,7 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_T
 
 <!-- *************************** PEANO ********************************* -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Peano/le.ind'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Peano/le.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:leq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -220,7 +220,7 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_T
     </m:apply>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/lt.con'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/lt.con'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:lt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -228,7 +228,7 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_T
     </m:apply>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/ge.con'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/ge.con'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:geq definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
@@ -236,7 +236,7 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/coq/INIT/Logic_T
     </m:apply>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Peano/gt.con'] and (count(child::*) = 3)]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/gt.con'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
     <m:gt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 486c0a43f..948cbbaec 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -101,14 +101,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <xsl:template match="APPLY" mode="pure">
    <xsl:choose>
-    <!-- <xsl:when test="//ALLTYPES and boolean(key('typeid',*/@id))"> -->
+    <!-- <xsl:when test="//InnerTypes and boolean(key('typeid',*/@id))"> -->
     <!-- start looking for subproofs -->
-    <xsl:when test="((*/@id) = (//ALLTYPES/TYPE/@id))"> 
+    <xsl:when test="((*/@id) = (//InnerTypes/TYPE/@of))"> 
      <m:apply helm:xref="{@id}">
       <m:csymbol>letin</m:csymbol>
       <!-- <xsl:for-each select="*[boolean(key('typeid',@id))]"> -->
       <!-- first process all subproofs (let-in) -->
-      <xsl:for-each select="*[@id = (//ALLTYPES/TYPE/@id)]">
+      <xsl:for-each select="*[@id = (//InnerTypes/TYPE/@of)]">
        <m:apply>
         <m:csymbol>let</m:csymbol>
         <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position())"/></xsl:with-param></xsl:call-template></m:ci>
@@ -140,7 +140,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
     <!-- <xsl:when test="key('typeid',@id)"> -->
-    <xsl:when test="//ALLTYPES/TYPE[@id=$id]">
+    <xsl:when test="//InnerTypes/TYPE[@of=$id]">
      <m:ci>
       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
      </m:ci>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index cd7593052..1d7945dc2 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -20,22 +20,22 @@
 
 <!-- Proof objects -->
 
-<!-- <xsl:key name="typeid" use="@id" match="TYPE"/> -->
+<!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
 
 <xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
   <xsl:choose> 
    <xsl:when test="@id">
     <xsl:variable name="id" select="@id"/>
     <xsl:choose>
-     <!-- <xsl:when test="//ALLTYPES and key('typeid',@id)"> -->
-     <xsl:when test="//ALLTYPES/TYPE[@id=$id]">
+     <!-- <xsl:when test="//InnerTypes and key('typeid',@id)"> -->
+     <xsl:when test="//InnerTypes/TYPE[@of=$id]">
      <xsl:choose>
       <xsl:when test="name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
        <m:apply helm:xref="{@id}">
         <m:csymbol>thread</m:csymbol>
-        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
         <m:apply>
          <m:csymbol>rw_step</m:csymbol>
          <xsl:apply-templates mode="pure" select="*[3]"/>
@@ -47,7 +47,7 @@
       </xsl:when>
       <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
       <xsl:when test="name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
  and count(child::*) = 6">
        <m:apply helm:xref="{@id}">
         <m:csymbol>and_ind</m:csymbol>
@@ -60,25 +60,25 @@
        </m:apply>
       </xsl:when>
       <xsl:when test="name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
  and count(child::*) = 7">
        <m:apply helm:xref="{@id}">
         <m:csymbol>or_ind</m:csymbol>
         <xsl:apply-templates mode="noannot" select="*[7]"/>
-        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
         <xsl:apply-templates mode="pure" select="*[5]"/>
         <xsl:apply-templates mode="pure" select="*[6]"/>
        </m:apply>
       </xsl:when>
-      <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
+      <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
        <m:apply helm:xref="{@id}">
         <m:csymbol>thread</m:csymbol>
-        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
         <m:apply>
          <m:csymbol>app</m:csymbol>
          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
         </m:apply>
-        <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
+        <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
        </m:apply>
       </xsl:when>
       <xsl:otherwise>
@@ -86,7 +86,7 @@
         <m:csymbol>proof</m:csymbol>
         <xsl:apply-templates select="." mode="pure"/>
         <!-- <xsl:apply-templates select="key('typeid',@id)" mode="pure"/> -->
-        <xsl:apply-templates select="//ALLTYPES/TYPE[@id=$id]" mode="pure"/>
+        <xsl:apply-templates select="//InnerTypes/TYPE[@of=$id]" mode="pure"/>
        </m:apply>
       </xsl:otherwise>
      </xsl:choose>
@@ -104,7 +104,7 @@
 
 <xsl:template match="*" mode="copy-of-no-prop">
  <xsl:choose>
-  <xsl:when test="@id = //ALLTYPES/TYPE/@id">
+  <xsl:when test="@id = //InnerTypes/TYPE/@of">
    <m:ci>previous</m:ci>
   </xsl:when>
   <xsl:otherwise>
@@ -117,10 +117,10 @@
 <xsl:template match="*" mode="thread">
   <xsl:choose>
    <xsl:when test="name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
     <xsl:variable name="id" select="@id"/>
-     <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+     <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
      <m:apply>
       <m:csymbol>rw_step</m:csymbol>
       <xsl:apply-templates mode="pure" select="*[3]"/>
@@ -131,24 +131,24 @@
    </xsl:when>
 <!--**** Patch temporanea, per il problema dei threads ***-->
 <xsl:when test="(name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
  and count(child::*) = 6) or
 (name()= 'APPLY' and CONST[
- attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
  and count(child::*) = 7)">
  <xsl:apply-templates mode="noannot" select="."/>
 </xsl:when>
 <!--**** Fine Patch temporanea, per il problema dei threads ***-->
-   <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
+   <xsl:when test="count(*[@id = //InnerTypes/TYPE/@of]) = 1">
        <xsl:variable name="id" select="@id"/>
        <m:apply helm:xref="{@id}">
         <m:csymbol>thread</m:csymbol>
-        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]"/>
         <m:apply>
          <m:csymbol>app</m:csymbol>
          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
         </m:apply>
-        <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
+        <xsl:apply-templates mode="thread" select="*[@id = //InnerTypes/TYPE/@of]"/>
        </m:apply>
    </xsl:when>
    <xsl:otherwise>
@@ -162,15 +162,15 @@
 
 <!-- non del tutto soddisfacente, ma .... -->
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/INIT/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/coq/ZARITH/auxiliary/eqT_ind_r.con']]" mode="appflat">
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con']]" mode="appflat">
     <xsl:choose>
      <xsl:when test="count(child::*) > 7">
       <xsl:variable name="id" select="@id"/>
       <xsl:variable name="ideqp" select="*[7]/@id"/>
       <xsl:variable name="idsubp" select="*[5]/@id"/>
-      <xsl:variable name="leteqp" select="boolean(//ALLTYPES/TYPE[@id=$ideqp])"/>
-      <xsl:variable name="letsubp" select="boolean(//ALLTYPES/TYPE[@id=$idsubp])"/>
+      <xsl:variable name="leteqp" select="boolean(//InnerTypes/TYPE[@of=$ideqp])"/>
+      <xsl:variable name="letsubp" select="boolean(//InnerTypes/TYPE[@of=$idsubp])"/>
       <m:apply helm:xref="{@id}">
        <m:csymbol>rewrite_and_apply</m:csymbol>
        <m:apply>
@@ -224,7 +224,7 @@
 </xsl:template> 
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con']]" mode="appflat">
+ attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
     <xsl:choose>
      <xsl:when test="count(child::*) > 4">
       <m:apply helm:xref="{@id}">
diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl
index ff69f9a22..4d17ae260 100644
--- a/helm/style/reals.xsl
+++ b/helm/style/reals.xsl
@@ -22,18 +22,18 @@
 <!-- REALS -->
 
 <!--
-<xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R.con']" mode="pure">
+<xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R.con']" mode="pure">
  <m:reals/>
 </xsl:template>
 -->
 
 <!-- 0 e 1 -->
 
-<xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R0.con']" mode="pure">
+<xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R0.con']" mode="pure">
  <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
 </xsl:template>
 
-<xsl:template match="CONST[attribute::uri='cic:/coq/REALS/Raxioms/R1.con']" mode="pure">
+<xsl:template match="CONST[attribute::uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="pure">
  <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
 </xsl:template>
 
@@ -42,24 +42,24 @@
 <!-- Unary Operations -->
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/REALS/Raxioms/Ropp.con' or
- attribute::uri='cic:/coq/REALS/Rbasic_fun/Rabsolu.con' or
- attribute::uri='cic:/coq/REALS/Rfunctions/fact.con' or
- attribute::uri='cic:/coq/REALS/Rbase/Rsqr.con']]" mode="pure">
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Ropp.con' or
+ attribute::uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con' or
+ attribute::uri='cic:/Coq/Reals/Rfunctions/fact.con' or
+ attribute::uri='cic:/Coq/Reals/Rbase/Rsqr.con']]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(child::*) = 2">
       <xsl:variable name="elem">
        <xsl:choose>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Ropp.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Ropp.con'">
          <xsl:value-of select="'minus'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbasic_fun/Rabsolu.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rabsolu.con'">
          <xsl:value-of select="'abs'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Rfunctions/fact.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rfunctions/fact.con'">
          <xsl:value-of select="'factorial'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbase/Rsqr.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbase/Rsqr.con'">
          <xsl:value-of select="'root'"/>
         </xsl:when>
        </xsl:choose>
@@ -83,7 +83,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/REALS/Raxioms/Rinv.con']]" mode="pure">
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rinv.con']]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(child::*) = 2">
       <m:apply helm:xref="{@id}">
@@ -111,44 +111,44 @@
 <!-- Binary Operations and Relations -->
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/REALS/Raxioms/Rplus.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rminus.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rmult.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rle.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rlt.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rge.con' or
- attribute::uri='cic:/coq/REALS/Raxioms/Rgt.con' or
- attribute::uri='cic:/coq/REALS/Rbasic_fun/Rmin.con' or
- attribute::uri='cic:/coq/REALS/Rfunctions/pow.con']]" mode="pure">
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rplus.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rminus.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rmult.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rle.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rlt.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rge.con' or
+ attribute::uri='cic:/Coq/Reals/Rdefinitions/Rgt.con' or
+ attribute::uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con' or
+ attribute::uri='cic:/Coq/Reals/Rfunctions/pow.con']]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(child::*) = 3">
       <xsl:variable name="elem">
        <xsl:choose>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rplus.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'">
          <xsl:value-of select="'plus'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rminus.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rminus.con'">
          <xsl:value-of select="'minus'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rmult.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rmult.con'">
          <xsl:value-of select="'times'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rle.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rle.con'">
          <xsl:value-of select="'leq'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rlt.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rlt.con'">
          <xsl:value-of select="'lt'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rge.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rge.con'">
          <xsl:value-of select="'geq'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Raxioms/Rgt.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rdefinitions/Rgt.con'">
          <xsl:value-of select="'gt'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Rbasic_fun/Rmin.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbasic_fun/Rmin.con'">
          <xsl:value-of select="'min'"/>
         </xsl:when>
-        <xsl:when test="CONST/@uri='cic:/coq/REALS/Rfunctions/pow.con'">
+        <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rfunctions/pow.con'">
          <xsl:value-of select="'power'"/>
         </xsl:when>
        </xsl:choose>
@@ -175,7 +175,7 @@
 <!-- LIMIT -->
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/REALS/Rlimit/limit1_in.con']]" mode="pure">
+ attribute::uri='cic:/Coq/Reals/Rlimit/limit1_in.con']]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(child::*) = 5">
       <m:apply>
@@ -229,7 +229,7 @@
 <!-- DIFFERENTIATION -->
 
 <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/coq/REALS/Rderiv/D_in.con']]" mode="pure">
+ attribute::uri='cic:/Coq/Reals/Rderiv/D_in.con']]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(child::*) = 4">
       <m:apply>
diff --git a/helm/style/ricerca.xsl b/helm/style/ricerca.xsl
index 28e210dca..03129b21c 100644
--- a/helm/style/ricerca.xsl
+++ b/helm/style/ricerca.xsl
@@ -26,10 +26,10 @@
 
 
 
-<xsl:template match="MUTIND[string(@uri)='cic:/coq/INIT/Logic/Equality/eq.ind']" mode="search" >
+<xsl:template match="MUTIND[string(@uri)='cic:/Coq/Init/Logic/Equality/eq.ind']" mode="search" >
 <!-- <xsl:param name="current_uri" select=""/> -->
 <!-- <h1><xsl:value-of select="string(@uri)"/></h1> -->
-<!-- <xsl:if test="string(@uri)='cic:/coq/INIT/Logic/Equality/eq.ind'"> -->
+<!-- <xsl:if test="string(@uri)='cic:/Coq/Init/Logic/Equality/eq.ind'"> -->
   <xsl:value-of select="$current_uri"/><BR/>
 <!-- </xsl:if> -->
 </xsl:template>
@@ -46,7 +46,7 @@
 <xsl:template match="VARIABLE">
 <!-- <xsl:param name="current_uri" select=""/> -->
 <xsl:variable name="found" 
-  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/coq/INIT/Logic/Equality/eq.ind'])"/>
+  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/Coq/Init/Logic/Equality/eq.ind'])"/>
 <xsl:if test="$found">
   <xsl:value-of select="concat(string($current_uri),&quot;/&quot;,string(@uri),&quot;.xml&quot;)"/><BR/>
 </xsl:if>
@@ -61,7 +61,7 @@
   <xsl:with-param name="current_uri" select="concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri))"/>
  </xsl:apply-templates> -->
 <xsl:variable name="found" 
-  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/coq/INIT/Logic/Equality/eq.ind'])"/>
+  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/Coq/Init/Logic/Equality/eq.ind'])"/>
 <xsl:if test="$found">
   <xsl:value-of select="concat(string($current_uri),&quot;/&quot;,string(@uri),&quot;.xml&quot;)"/><BR/>
 </xsl:if>
@@ -73,7 +73,7 @@
   <xsl:with-param name="current_uri" select="concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri))"/>
  </xsl:apply-templates> -->
 <xsl:variable name="found" 
-  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/coq/INIT/Logic/Equality/eq.ind'])"/>
+  select="boolean(document(concat(string($absPath),string($current_uri),&quot;/&quot;,string(@uri)))//MUTIND[string(@uri)='cic:/Coq/Init/Logic/Equality/eq.ind'])"/>
 <xsl:if test="$found">
   <xsl:value-of select="concat(string($current_uri),&quot;/&quot;,string(@uri),&quot;.xml&quot;)"/><BR/>
 </xsl:if>
diff --git a/helm/style/set.xsl b/helm/style/set.xsl
index 916a92c51..4a29f4678 100644
--- a/helm/style/set.xsl
+++ b/helm/style/set.xsl
@@ -46,7 +46,7 @@
 
 <!-- IN -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -71,8 +71,8 @@
 
 <!-- NOT-IN -->
 <!-- NOT ha no parameters -->
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
-and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
+and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -96,7 +96,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- EMPTY SET -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -110,7 +110,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 2">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
        </m:set>
@@ -124,7 +124,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SINGLETON -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -139,7 +139,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 3">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -154,7 +154,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- COUPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Couple.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -170,7 +170,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 4">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -186,7 +186,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- TRIPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -203,7 +203,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
      </xsl:when>   
      <xsl:when test="(count(child::*) - number($no_params)) = 5">
       <m:apply helm:xref="{@id}">
-       <m:in definitionURL="cic:/coq/SETS/Ensembles/Ensembles/In.con"/>
+       <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
        <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
        <m:set definitionURL="{MUTIND/@uri}">
         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
@@ -220,7 +220,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- INTERSECTION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -255,7 +255,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- UNION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Union.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -289,7 +289,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Included.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -312,7 +312,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- STRICTLY INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -335,7 +335,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SET-DIFF -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Setminus.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -369,7 +369,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- ADD-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Add.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -407,7 +407,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SUBTRACT-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Subtract.con']]" mode="pure">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -445,7 +445,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- CARD -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>