X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_proof.xsl;h=b699ed402ad8f163c511517d2f9cfb90669708ce;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=343cafd637e42a64880cd33cd7e550422e3e4397;hpb=734a6fc5d8da4896c646d1dd7a17afaf0dd33224;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index 343cafd63..b699ed402 100644
--- a/helm/nuprl_stylesheets/nuprl_proof.xsl
+++ b/helm/nuprl_stylesheets/nuprl_proof.xsl
@@ -15,6 +15,12 @@
   </Definition>
 </xsl:template>
 
+<xsl:template match="NuPrlDefinition">
+ <NuPrlDefinition>
+  <xsl:apply-templates select="*"/>
+ </NuPrlDefinition>
+</xsl:template>
+
 <xsl:template match="node">
   <xsl:element name="Node">
     <xsl:apply-templates/>
@@ -54,15 +60,7 @@
 </xsl:template>
 
 <xsl:template match="tacticinstance">
-  <TacticInstance name="{@name}">
-    <xsl:apply-templates select="extra_info"/>
-  </TacticInstance>
-</xsl:template>
-
-<xsl:template match="extra_info">
- <extra_info>
-  <xsl:copy-of select="*|@*|text()"/>
- </extra_info>
+  <TacticInstance name="{@name}" uri="{@uri}"/>
 </xsl:template>
 
 <xsl:template match="tacticproof">