From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 Apr 2003 17:05:40 +0000 (+0000)
Subject: extra_info hack removed
X-Git-Tag: before_refactoring~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8bd6f1c6b48b2d3ba90ed6e9bb645b03d752407b;p=helm.git

extra_info hack removed
---

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
index 5fb0c0d8a..43d420f2f 100644
--- a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
+++ b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
@@ -2785,10 +2785,6 @@
           </xsl:call-template>
           <xsl:text>By </xsl:text>
           <xsl:apply-templates select="TacticInstance/@name"/>
-          <!-- CSC: extra_info in HTML to be rendered here -->
-          <xsl:for-each select="TacticInstance/extra_info">
-           <xsl:copy-of select="*|text()"/>
-          </xsl:for-each>
           <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
           <xsl:if test="$explode_tactics">
 	   <span ID="{$freshid4}">
diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index 8ba633db6..f6eb2a7c0 100644
--- 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">