]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/dtd/cic.dtd
ocaml 3.09 transition
[helm.git] / helm / dtd / cic.dtd
index 840f797f60bee29d92985f19654b303c1a7f7503..28f2804f92d7110b4f9c9b81daa4b772ea6af9fb 100644 (file)
           no  NMTOKEN #REQUIRED
           id  ID      #REQUIRED>
 
-<!ELEMENT attributes EMPTY>
-<!ATTLIST attributes
-          class (coercion|elimProp|elimCProp|elimSet|elimType|record|projection) #IMPLIED
-          generated   (true|false)  #IMPLIED>
+<!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: -->