<!-- 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
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*)>
<!ELEMENT IMPLICIT EMPTY>
<!ATTLIST IMPLICIT
- id ID #REQUIRED>
+ id ID #REQUIRED
+ annotation (closed|type|hole) #IMPLIED>
<!ELEMENT CONST EMPTY>
<!ATTLIST CONST