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

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 97e6cd6b1..28f2804f9 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,16 @@
           no  NMTOKEN #REQUIRED
           id  ID      #REQUIRED>
 
+<!ELEMENT attributes ((class,generated?)|(generated,class?))?>
+
+<!ELEMENT generated EMPTY>
+
+<!-- the fields are allowed only when @value = "record"
+     the SORT is allowed only when @value = "elim" -->
+<!ELEMENT class (field*|SORT)>
+<!ATTLIST class
+          value (coercion|elim|record|projection) #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -139,7 +149,8 @@
 
 <!ELEMENT IMPLICIT EMPTY>
 <!ATTLIST IMPLICIT
-          id ID #REQUIRED>
+          id ID #REQUIRED
+	  annotation (closed|type|hole) #IMPLIED>
 
 <!ELEMENT CONST EMPTY>
 <!ATTLIST CONST