Params is now a list of Param.

[helm.git] / helm / dtd / cicobject.dtd

diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd
index 9514103e45339159e9a2aa7a11db719a2a660879..b534e373cb902f065634c195e272b4520a9b7aa6 100644 (file)
--- 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*)>
@@ -86,7 +90,21 @@
 <!ATTLIST Param
           name CDATA #REQUIRED>
 
-<!ELEMENT Params (#PCDATA)*>
+<!ELEMENT Params (Param)*>
+
+<!ELEMENT Param (CDATA)*>
+<!ATTLIST Param
+          definitionURL CDATA #REQUIRED>
+
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
 
 <!-- Sintactic sugar for CIC objects: -->