extra_info hack removed

[helm.git] / helm / nuprl_stylesheets / nuprl_proof.xsl

diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index 8ba633db6c378b8fc16beb735a3f49dbdbc3474b..f6eb2a7c095220935e52aacddab4257a48983bd0 100644 (file)
--- a/helm/nuprl_stylesheets/nuprl_proof.xsl
+++ b/helm/nuprl_stylesheets/nuprl_proof.xsl
@@ -54,15 +54,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">