X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fdtd%2Fcicobject.dtd;h=10f001df645f8e0ea6bc1c6e585a6ad3f15f96c5;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a6b6155b1f156db72c17bb8e24f67c4a88183b34;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git

diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd
index a6b6155b1..10f001df6 100644
--- a/helm/dtd/cicobject.dtd
+++ b/helm/dtd/cicobject.dtd
@@ -62,11 +62,15 @@
 <!ATTLIST InductiveDefinition
           xmlns:m    CDATA      #REQUIRED>
 
-<!ELEMENT Variable (type)>
+<!ELEMENT Variable (body?,type)>
 <!ATTLIST Variable
           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,19 @@
 <!ATTLIST Param
           name CDATA #REQUIRED>
 
-<!ELEMENT Params (#PCDATA)*>
+<!ELEMENT Params (param)*>
+
+<!ELEMENT param %term;>
+
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
 
 <!-- Sintactic sugar for CIC objects: -->