X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fdtd%2Fcic.dtd;h=28f2804f92d7110b4f9c9b81daa4b772ea6af9fb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=840f797f60bee29d92985f19654b303c1a7f7503;hpb=cb379a463ec772df8855310fc9bf7276ea5f3f3d;p=helm.git

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 840f797f6..28f2804f9 100644
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -52,10 +52,15 @@
           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: -->