From: Matteo Selmi <matteo.selmi@mail.polimi.it>
Date: Tue, 22 Oct 2002 14:25:56 +0000 (+0000)
Subject: - removed checkings for objects Definition and Axiom.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b72beb68cf0c34cb0785ad7e2a4c426494e29e6a;p=helm.git

- removed checkings for objects Definition and Axiom.
- inserted checkings for objects CostantType and ConstantBody.
- modified mode of view params (not "path/varname.var" but "varname").
- modified checkings for term LAMBDA, LETIN, PROD (with insertion of checkings for decl and def when used by these terms)
---

diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl
index 97f259d67..2f5fa84e6 100644
--- a/helm/style/annotatedcont.xsl
+++ b/helm/style/annotatedcont.xsl
@@ -35,9 +35,9 @@
 
 <xsl:import href="objcontent.xsl"/>
 
-<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable"/>
 
-<xsl:template match="Definition|Axiom|CurrentProof|InductiveDefinition|Variable">
+<xsl:template match="ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable">
     <xsl:variable name="id" select="@id"/>
     <xsl:choose>
     <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl
index a9d82ddac..bdb4ae3eb 100644
--- a/helm/style/basic.xsl
+++ b/helm/style/basic.xsl
@@ -39,9 +39,9 @@
 
 <!-- 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/and.ind'] and (count(child::*) = 3)]" mode="pure">
     <m:apply helm:xref="{@id}">
-    <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
+     <m:and definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
      <xsl:apply-templates select="*[2]" mode="noannot"/>
      <xsl:apply-templates select="*[3]" mode="noannot"/>
     </m:apply>
@@ -49,7 +49,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/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"/>
@@ -79,7 +79,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/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>
@@ -109,7 +109,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/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>
@@ -176,7 +176,7 @@
 
 <!-- EQUALITY and TYPE EQUALITY -->
 
-<xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Logic/Equality/eq.ind']" mode="pure">
+<xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Logic/eq.ind']" mode="pure">
    <xsl:call-template name="mk-mml-op-noannot">
       <xsl:with-param name="hide" select="1"/>
       <xsl:with-param name="c-tag" select="MUTIND"/>
@@ -195,7 +195,7 @@
 <!-- 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">
+and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic/eq.ind']]]" mode="pure">
     <xsl:choose>
      <xsl:when test="count(APPLY/child::*) = 4">
       <m:apply helm:xref="{@id}">
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index e60a85051..d557cb5e8 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -62,21 +62,62 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <!-- CIC TERMS -->
 
-<xsl:template match="LAMBDA" mode="pure">
-    <m:lambda helm:xref="{@id}">
+<!--xsl:template match="LAMBDA" mode="pure">
+    <m:lambda helm:xref="{decl/@id}">
      <m:bvar>
       <m:ci>
-       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
+       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="decl/@binder"/></xsl:with-param></xsl:call-template>
       </m:ci>
       <m:type>
-       <xsl:apply-templates select="source/*[1]" mode="noannot"/>
+       <xsl:apply-templates select="decl/*[1]" mode="noannot"/>
       </m:type>
      </m:bvar>
      <xsl:apply-templates select="target/*[1]" mode="noannot"/>
     </m:lambda>
+</xsl:template-->
+
+<!--xsl:template match="LAMBDA" mode="pure">
+	<xsl:for-each select="decl">
+	 <m:lambda helm:xref="{@id}">
+	  <m:bvar>
+	   <m:ci>
+	    <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+	   </m:ci>
+	   <m:type>
+	    <xsl:apply-templates select="*[1]" mode="noannot"/>
+           </m:type>
+	  </m:bvar>
+	 </m:lambda>
+	</xsl:for-each>
+	<xsl:apply-templates select="target/*[1]" mode="noannot"/-->
+	 <!--xsl:for-each select="decl">
+	  </m:lambda>
+	 </xsl:for-each-->
+<!--/xsl:template-->
+
+<xsl:template match="LAMBDA" mode="pure">
+	<xsl:apply-templates select="*[1]" mode="lambda"/>
 </xsl:template>
 
-<xsl:template match="LETIN" mode="pure">
+<xsl:template match="decl" mode="lambda">
+	<m:lambda helm:xref="{@id}">
+	 <m:bvar>
+	  <m:ci>
+	   <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+	  </m:ci>
+	  <m:type>
+	   <xsl:apply-templates select="*[1]" mode="noannot"/>
+          </m:type>
+	 </m:bvar>
+	<xsl:apply-templates select="following-sibling::*[1]" mode="lambda"/>
+	</m:lambda>
+</xsl:template>
+
+<xsl:template match="target" mode="lambda">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!--xsl:template match="LETIN" mode="pure">
     <m:apply helm:xref="{@id}">
      <m:csymbol>let_in</m:csymbol>
      <m:bvar>
@@ -87,36 +128,98 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
      <xsl:apply-templates select="*[1]" mode="noannot"/>
      <xsl:apply-templates select="letintarget/*[1]" mode="noannot"/>
     </m:apply>
+</xsl:template-->
+
+<xsl:template match="LETIN" mode="pure">
+	<xsl:apply-templates select="*[1]" mode="letin"/>
 </xsl:template>
 
-<xsl:template match="PROD" mode="pure">
+<xsl:template match="def" mode="letin">	
     <m:apply helm:xref="{@id}">
-     <xsl:choose>
-     <xsl:when test="string(target/@binder)= &quot;&quot;">
-      <m:csymbol>arrow</m:csymbol>
-      <xsl:apply-templates select="source/*[1]" mode="noannot"/>
-     </xsl:when>
-     <xsl:otherwise>
+     <m:csymbol>let_in</m:csymbol>
+     <m:bvar>
+      <m:ci>
+       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+      </m:ci>
+     </m:bvar>
+     <xsl:apply-templates select="*[1]" mode="noannot"/>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="letin"/>
+    </m:apply>
+</xsl:template>
+
+<xsl:template match="target" mode="letin">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!--xsl:template match="PROD" mode="pure">
+    <xsl:for-each select="decl">
+     <m:apply helm:xref="{@id}">
       <xsl:choose>
-       <xsl:when test="@type = 'Prop'">
-        <m:csymbol>forall</m:csymbol>
+       <xsl:when test="string(@binder)= &quot;&quot;">
+        <m:csymbol>arrow</m:csymbol>
+        <xsl:apply-templates select="*[1]" mode="noannot"/>
        </xsl:when>
        <xsl:otherwise>
-        <m:csymbol>prod</m:csymbol>
+        <xsl:choose>
+         <xsl:when test="../@type = 'Prop'">
+          <m:csymbol>forall</m:csymbol>
+         </xsl:when>
+         <xsl:otherwise>
+          <m:csymbol>prod</m:csymbol>
+         </xsl:otherwise>
+        </xsl:choose>
+        <m:bvar>
+         <m:ci>
+          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+         </m:ci>
+         <m:type>
+          <xsl:apply-templates select="*[1]" mode="noannot"/>
+         </m:type>
+        </m:bvar>
        </xsl:otherwise>
       </xsl:choose>
-       <m:bvar>
-        <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
-        </m:ci>
-        <m:type>
-         <xsl:apply-templates select="source/*[1]" mode="noannot"/>
-        </m:type>
-       </m:bvar>
-     </xsl:otherwise>
-     </xsl:choose>
-     <xsl:apply-templates select="target/*[1]" mode="noannot"/>
-    </m:apply>
+     </m:apply>
+    </xsl:for-each>
+    <xsl:apply-templates select="target/*[1]" mode="noannot"/> 
+</xsl:template-->
+
+<xsl:template match="PROD" mode="pure">
+	<xsl:apply-templates select="*[1]" mode="prod"/>
+</xsl:template>
+
+<xsl:template match="decl" mode="prod">
+     <m:apply helm:xref="{@id}">
+      <xsl:choose>
+       <xsl:when test="string(@binder)= &quot;&quot;">
+        <m:csymbol>arrow</m:csymbol>
+        <xsl:apply-templates select="*[1]" mode="noannot"/>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:choose>
+         <xsl:when test="../@type = 'Prop'">
+          <m:csymbol>forall</m:csymbol>
+         </xsl:when>
+         <xsl:otherwise>
+          <m:csymbol>prod</m:csymbol>
+         </xsl:otherwise>
+        </xsl:choose>
+        <m:bvar>
+         <m:ci>
+          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+         </m:ci>
+         <m:type>
+          <xsl:apply-templates select="*[1]" mode="noannot"/>
+         </m:type>
+        </m:bvar>
+       </xsl:otherwise>
+      </xsl:choose>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="prod"/> 
+     </m:apply>
+</xsl:template>
+
+	 
+<xsl:template match="target" mode="prod">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
 <xsl:template match="CAST" mode="pure">
@@ -163,7 +266,10 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <xsl:template match="VAR" mode="pure">
     <m:ci helm:xref="{@id}">
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="substring-after(@relUri,&quot;,&quot;)"/></xsl:with-param></xsl:call-template>
+     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri_bis">
+          <xsl:with-param name="uri" select="@uri"/>
+	      </xsl:call-template>
+	      </xsl:with-param></xsl:call-template>
     </m:ci>
 </xsl:template>
 
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index ceb7a22ba..9cf2ca7f9 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -52,6 +52,51 @@
     <xsl:apply-templates select="*[1]"/>
 </xsl:template>
 
+
+<!-- FUNZIONI AUSILIARIE -->
+
+<xsl:template name="name_of_uri_bis">
+ <xsl:param name="uri" select="&quot;&quot;"/>
+  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
+  <xsl:choose>
+   <xsl:when test="$suffix = &quot;&quot;">
+    <xsl:value-of select="substring-before($uri,&quot;.var&quot;)"/>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:call-template name="name_of_uri_bis">
+     <xsl:with-param name="uri" select="$suffix"/>
+    </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template name="var_name">
+ <xsl:param name="uri"/>
+ <xsl:param name="string" select="&quot;&quot;"/>
+  <xsl:variable name="prefix" select="substring-before($uri, &quot; &quot;)"/>
+  <xsl:variable name="suffix" select="substring-after($uri, &quot; &quot;)"/> 
+  <xsl:variable name="prefix">
+   <xsl:call-template name="name_of_uri_bis">
+    <xsl:with-param name="uri" select="$prefix"/>
+   </xsl:call-template>
+  </xsl:variable> 
+  <!--xsl:if test="string($prefix) != &quot; &quot; "-->
+   <xsl:variable name="string" select="concat($string,', ', $prefix)"/>
+  <!--/xsl:if-->
+  <xsl:choose>
+   <xsl:when test="$suffix = &quot;&quot;">
+   <xsl:value-of select="substring-after(concat($string, ' '),',')"/>
+   </xsl:when>
+   <xsl:otherwise>
+   <xsl:call-template name="var_name">
+    <xsl:with-param name="uri" select="$suffix"/>
+    <xsl:with-param name="string" select="$string"/>
+   </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+				  
+				  
 <!-- CIC OBJECTS -->
 
 <xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
@@ -73,11 +118,13 @@
     </Sequent> 
 </xsl:template>
 
-<xsl:template match="Definition" mode="noannot">
+<xsl:template match="ConstantType" mode="noannot">
     <Definition name="{@name}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
       <Params>
-       <xsl:value-of select="@params"/>
+      <xsl:call-template name="var_name">
+       <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+      </xsl:call-template>
       </Params>
      </xsl:if>
 <!--     <xsl:choose>
@@ -92,35 +139,37 @@
        </body>
       </xsl:otherwise>
      </xsl:choose> -->
-     <body>
-      <xsl:apply-templates select="body/*[1]"/>
-     </body>
+     <body/>
      <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="./*[1]"/>
      </type>
     </Definition> 
 </xsl:template>
 
-<xsl:template match="Axiom" mode="noannot"> 
-    <Axiom name="{@name}" helm:xref="{@id}">
+<xsl:template match="ConstantBody" mode= "noannot">
+    <Definition name="{@for}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
       <Params>
-       <xsl:value-of select="@params"/>
+       <xsl:call-template name="var_name">
+       <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+       </xsl:call-template>
       </Params>
      </xsl:if>
-     <type>
-       <xsl:apply-templates select="type/*[1]"/>
-     </type>
-    </Axiom> 
+     <body>
+      <xsl:apply-templates select="./*[1]"/>
+     </body>
+     <type/>
+    </Definition>
 </xsl:template>
 
+
 <xsl:template match="CurrentProof" mode="noannot">
-    <CurrentProof name="{@name}" helm:xref="{@id}">
+    <CurrentProof name="{@of}" helm:xref="{@id}">
      <xsl:for-each select="Conjecture">
       <Conjecture no="{@no}" helm:xref="{@id}">
         <xsl:for-each select="*">
          <xsl:copy>
-          <xsl:copy-of select="@name"/>
+          <xsl:copy-of select="@of"/>
           <xsl:attribute name="helm:xref">
            <xsl:value-of select="@id"/>
           </xsl:attribute>
@@ -132,9 +181,6 @@
      <body>
        <xsl:apply-templates select="body/*[1]"/>
      </body>
-     <type>
-       <xsl:apply-templates select="type/*[1]"/>
-     </type>
     </CurrentProof> 
 </xsl:template>
 
diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl
index 7d890d611..a4937460a 100644
--- a/helm/style/objtheorycontent.xsl
+++ b/helm/style/objtheorycontent.xsl
@@ -33,7 +33,7 @@
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
-<xsl:import href="objcontent.xsl"/>
+<!--xsl:import href="objcontent.xsl"/-->
 <xsl:include href="headercontent.xsl"/>
 <xsl:include href="getter.xsl"/>
 
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index f61cbe6d9..82f2fd317 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -41,7 +41,7 @@
 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
 <xsl:key name="typeid" use="@of" match="TYPE"/>
 
-<!-- ALL this elements does not have inner type -->
+<!-- These elements do not have inner type -->
 <xsl:template match="PROD|SORT|MUTIND" mode="noannot">
  <xsl:apply-templates select="." mode="pure"/>
 </xsl:template>
@@ -59,10 +59,10 @@
  </xsl:variable>
  <xsl:choose>
   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+   <!--xsl:when test="@sort='Prop'"-->
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
-    <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
@@ -78,7 +78,7 @@
 
 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
 <xsl:template match="LAMBDA" mode="noannot">
- <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="id" select="decl/@id"/>
  <xsl:variable name="innertype_available">
   <xsl:for-each select="$InnerTypes">
    <xsl:if test="key('typeid',$id)/*">
@@ -86,9 +86,10 @@
    </xsl:if>
   </xsl:for-each>
  </xsl:variable>
+ <!--xsl:value-of select="concat('NL: ',$naturalLanguage,'  IA:  ',$innertype_available)"/-->
  <xsl:choose>
   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
-   <m:apply helm:xref="{@id}">
+   <m:apply helm:xref="{decl/@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
     <xsl:for-each select="$InnerTypes">
@@ -110,7 +111,6 @@
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
-    <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
@@ -611,28 +611,27 @@
     <!-- gestire meglio il caso di and_ind quando la prova 
          non e' della forma \x.\y.M -->
     <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] 
  and count(child::*) = 6 
- and name(*[5])='LAMBDA' 
- and name(*[5]/target/*[1])='LAMBDA'"> 
+ and name(*[5])='LAMBDA'"> 
       <m:apply helm:xref="{@id}">
        <m:csymbol>and_ind</m:csymbol>
        <xsl:apply-templates mode="noannot" select="*[6]"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
-       <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/> 
+       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+       <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+       <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
+       <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/> 
       </m:apply>
     </xsl:when>
     <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con'] 
+ attribute::uri='cic:/Coq/Init/Logic/or_ind.con'] 
  and count(child::*) = 7">
       <xsl:choose>
        <xsl:when test="name(*[5])='LAMBDA' 
                  and name(*[6])='LAMBDA'">
         <xsl:variable name="definition_url" 
-            select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
+            select="'cic:/Coq/Init/Logic/or.ind'"/>
         <m:apply helm:xref="{@id}">
          <m:csymbol>full_or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index 64acead36..74d29d9f3 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -40,7 +40,7 @@
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
 
 <!--******************************************************************-->
-<!-- Variable containing the absolute path of the CIC file            -->
+<!-- Variablie containing the absolute path of the CIC file            -->
 <!--******************************************************************-->
 
 <xsl:import href="annotatedcont.xsl"/>
@@ -53,8 +53,22 @@
 <xsl:param name="annotations" select="'no'"/>
 <xsl:param name="CICURI" select="''"/>
 
-<xsl:variable name="InnerTypesUri"><xsl:value-of select="concat($CICURI,'.types')"/></xsl:variable>
-<xsl:variable name="AnnotationsUri"><xsl:value-of select="concat($CICURI,'.ann')"/></xsl:variable>
+<!-- CSC: Wrong: we assume that no '.body' can appear in the middle of the URI -->
+<xsl:variable name="BaseCICURI">
+ <xsl:variable name="res" select="substring-before($CICURI,'.body')"/>
+ <xsl:choose>
+  <xsl:when test="$res = ''">
+   <xsl:value-of select="$CICURI"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="$res"/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:variable>
+
+<xsl:variable name="InnerTypesUri"><xsl:value-of select="concat($BaseCICURI,'.types')"/></xsl:variable>
+<!-- CSC: ?????????????????? -->
+<xsl:variable name="AnnotationsUri"><xsl:value-of select="concat($BaseCICURI,'.ann')"/></xsl:variable>
 
 <xsl:variable name="InnerTypesUrl"><xsl:call-template name="makeURL4InnerTypes"><xsl:with-param name="uri" select="$InnerTypesUri"/></xsl:call-template></xsl:variable>
 <xsl:variable name="AnnotationsUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$AnnotationsUri"/></xsl:call-template></xsl:variable>
@@ -67,7 +81,5 @@
 <xsl:include href="headercontent.xsl"/>
 <xsl:include href="proofs.xsl"/>
 <xsl:include href="inductive.xsl"/>
-
 <xsl:variable name="showproof" select="0"/>
-
 </xsl:stylesheet>