X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6ab6ffe1fcfbc51f201b94adcee89a14ff22d278;hb=1cfcea66d7394a785ec439cd6b03497b276918c4;hp=7aeec143f15f8a2cf3b11cbb934ae7aa900fee91;hpb=ddce32beebecf9d965e6ad991a08368f52cd9ea1;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 7aeec143f..6ab6ffe1f 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -181,12 +181,12 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:for-each select="Conjecture">
       <m:mtr>
        <m:mtd>
-        <m:mrow>
+        <m:mrow helm:xref="{@helm:xref}">
          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
          <xsl:for-each select="Decl|Def|Hidden">
           <xsl:choose>
            <xsl:when test="name(.)='Decl'">
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <xsl:choose>
               <xsl:when test="@name">
                <m:mi><xsl:value-of select="@name"/></m:mi>
@@ -200,7 +200,7 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </xsl:when>
            <xsl:when test="name(.)='Def'">
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <xsl:choose>
               <xsl:when test="@name">
                <m:mi><xsl:value-of select="@name"/></m:mi>
@@ -214,7 +214,7 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </xsl:when>
            <xsl:otherwise>
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <m:mi>_</m:mi>
              <m:mo>:?</m:mo>
              <m:mi>_</m:mi>
@@ -424,7 +424,7 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:for-each select="Decl|Def">
        <m:mtr>
         <m:mtd>
-         <m:mrow>
+         <m:mrow helm:xref="{@helm:xref}">
           <m:mi><xsl:value-of select="@name"/></m:mi>
           <xsl:choose>
            <xsl:when test="name(.) = 'Decl'">