- the mathql interpreter is not helm-dependent any more

[helm.git] / helm / style / objcontent.xsl
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl

index aef9daa6b666828280ec4a2b6bf1b8302c37f74b..ceb7a22bacea1b6818a37540ac0ad87c09534d01 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -55,12 +55,15 @@
  <!-- CIC OBJECTS -->
  
  <xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
-    <Sequent helm:xref="{@id}">
-     <xsl:for-each select="Declaration|Definition">
+    <Sequent helm:xref="{@id}" no="{@no}">
+     <xsl:for-each select="Decl|Def|Hidden">
        <xsl:copy>
         <xsl:attribute name="name">
          <xsl:value-of select="@name"/>
         </xsl:attribute>
+       <xsl:attribute name="helm:xref">
+        <xsl:value-of select="@id"/>
+       </xsl:attribute>
         <xsl:apply-templates select="*[1]"/>
        </xsl:copy>
       </xsl:for-each>
@@ -114,8 +117,16 @@
  <xsl:template match="CurrentProof" mode="noannot">
      <CurrentProof name="{@name}" helm:xref="{@id}">
       <xsl:for-each select="Conjecture">
-      <Conjecture no="{@no}">
-        <xsl:apply-templates select="."/>
+      <Conjecture no="{@no}" helm:xref="{@id}">
+        <xsl:for-each select="*">
+         <xsl:copy>
+          <xsl:copy-of select="@name"/>
+          <xsl:attribute name="helm:xref">
+           <xsl:value-of select="@id"/>
+          </xsl:attribute>
+          <xsl:apply-templates select="*"/>
+         </xsl:copy>
+        </xsl:for-each>
        </Conjecture>
       </xsl:for-each>
       <body>