X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_proof.xsl;h=b699ed402ad8f163c511517d2f9cfb90669708ce;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8ba633db6c378b8fc16beb735a3f49dbdbc3474b;hpb=e9db2c226034b75e69dba72b6bd577a7bcf6a31f;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index 8ba633db6..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}" uri="{@uri}">
-    <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">