From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2002 12:54:19 +0000 (+0000)
Subject: Declaration and Definition renamed to Decl and Def because
X-Git-Tag: V_0_3_0_debian_8~174
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f0d6e8932f4200a6b1956995225211df2a271a8;p=helm.git

Declaration and Definition renamed to Decl and Def because
Definition was already defined in the DTD.
---

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"/>