Declaration and Definition renamed to Decl and Def because

[helm.git] / helm / dtd / cic.dtd

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 0a90d9e908fe367780af3bfc0a7d2b418ccca933..a2156a522b507c96a92adf72d9f2605c99a49681 100644 (file)
--- 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)>