X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fdtd%2Fcic.dtd;h=840f797f60bee29d92985f19654b303c1a7f7503;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=97e6cd6b1239cf29dfdc9a185d5dc32eb05419e2;hpb=8f4249c2d863e08279ecfd6926a805ad242038c4;p=helm.git

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 97e6cd6b1..840f797f6 100644
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -18,30 +18,30 @@
 <!-- CIC objects: -->
 
 <!-- CSC: so far params is equal to the one of the only body.  -->
-<!ELEMENT ConstantType %term;>
+<!ELEMENT ConstantType (attributes?,%term;)>
 <!ATTLIST ConstantType
           name       CDATA      #REQUIRED
           params     CDATA      #REQUIRED
           id         ID         #REQUIRED>
 
-<!ELEMENT ConstantBody %term;>
+<!ELEMENT ConstantBody (attributes?,%term;)>
 <!ATTLIST ConstantBody
           for        CDATA      #REQUIRED
           params     CDATA      #REQUIRED
           id         ID         #REQUIRED>
 
-<!ELEMENT CurrentProof (Conjecture*,body)>
+<!ELEMENT CurrentProof (attributes?,Conjecture*,body)>
 <!ATTLIST CurrentProof
           of         CDATA      #REQUIRED
           id         ID         #REQUIRED>
 
-<!ELEMENT InductiveDefinition (InductiveType+)>
+<!ELEMENT InductiveDefinition (attributes?,InductiveType+)>
 <!ATTLIST InductiveDefinition
           noParams NMTOKEN #REQUIRED
           params   CDATA   #REQUIRED
           id       ID      #REQUIRED>
 
-<!ELEMENT Variable (body?,type)>
+<!ELEMENT Variable (attributes?,body?,type)>
 <!ATTLIST Variable
           name   CDATA #REQUIRED
           params CDATA #REQUIRED
@@ -52,6 +52,11 @@
           no  NMTOKEN #REQUIRED
           id  ID      #REQUIRED>
 
+<!ELEMENT attributes EMPTY>
+<!ATTLIST attributes
+          class (coercion|elimProp|elimCProp|elimSet|elimType|record|projection) #IMPLIED
+          generated   (true|false)  #IMPLIED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -139,7 +144,8 @@
 
 <!ELEMENT IMPLICIT EMPTY>
 <!ATTLIST IMPLICIT
-          id ID #REQUIRED>
+          id ID #REQUIRED
+	  annotation (closed|type|hole) #IMPLIED>
 
 <!ELEMENT CONST EMPTY>
 <!ATTLIST CONST