From 1f0d6e8932f4200a6b1956995225211df2a271a8 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2002 12:54:19 +0000
Subject: [PATCH] Declaration and Definition renamed to Decl and Def because
 Definition was already defined in the DTD.

---
 helm/dtd/cic.dtd            | 14 ++++++++++++++
 helm/dtd/cicobject.dtd      | 14 ++++++++++++++
 helm/style/mmlextension.xsl |  8 ++++----
 helm/style/objcontent.xsl   |  2 +-
 4 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 0a90d9e90..a2156a522 100644
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -74,6 +74,10 @@
           name CDATA #REQUIRED
           id   ID    #REQUIRED>
 
+<!ELEMENT Sequent ((Decl|Def)*,Goal)>
+<!ATTLIST Sequent
+          id   ID    #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -89,6 +93,16 @@
 <!ATTLIST Constructor
           name CDATA #REQUIRED>
 
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
 <!-- CIC terms: -->
 
 <!ELEMENT LAMBDA (source,target)>
diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd
index 9514103e4..d78251c1d 100644
--- a/helm/dtd/cicobject.dtd
+++ b/helm/dtd/cicobject.dtd
@@ -67,6 +67,10 @@
           name CDATA #REQUIRED
           xmlns:m    CDATA      #REQUIRED>
 
+<!ELEMENT Sequent ((Decl|Def)*,Goal)>
+<!ATTLIST Sequent
+          id   ID    #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -88,6 +92,16 @@
 
 <!ELEMENT Params (#PCDATA)*>
 
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
 <!-- Sintactic sugar for CIC objects: -->
 
 <!ELEMENT type  %term;>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 65a2b4612..6e766e352 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -365,7 +365,7 @@ which generates the toplevel element (see for instance xlink) -->
 
 <xsl:template match="Sequent">
  <xsl:variable name="rowlines">
-  <xsl:for-each select="Declaration|Definition">
+  <xsl:for-each select="Decl|Def">
    <xsl:if test="position() != last()">
     <xsl:text>none </xsl:text>
    </xsl:if>
@@ -374,13 +374,13 @@ which generates the toplevel element (see for instance xlink) -->
  </xsl:variable>
     <m:math>
      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
-      <xsl:for-each select="Declaration|Definition">
+      <xsl:for-each select="Decl|Def">
        <m:mtr>
         <m:mtd>
          <m:mrow>
           <m:mi><xsl:value-of select="@name"/></m:mi>
           <xsl:choose>
-           <xsl:when test="name(.) = 'Declaration'">
+           <xsl:when test="name(.) = 'Decl'">
             <m:mo>:</m:mo>
            </xsl:when>
            <xsl:otherwise>
@@ -392,7 +392,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtd>
        </m:mtr>
       </xsl:for-each>
-      <xsl:if test="not(Declaration|Definition)">
+      <xsl:if test="not(Decl|Def)">
       <m:mtr>
        <m:mtd>
         <m:mrow>
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index aef9daa6b..898e41a98 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -56,7 +56,7 @@
 
 <xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
     <Sequent helm:xref="{@id}">
-     <xsl:for-each select="Declaration|Definition">
+     <xsl:for-each select="Decl|Def">
       <xsl:copy>
        <xsl:attribute name="name">
         <xsl:value-of select="@name"/>
-- 
2.39.2