From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 15 Jun 2005 16:49:53 +0000 (+0000)
Subject: Syntax of <attributes>...</attributes> improved to allow arguments for
X-Git-Tag: INDEXING_NO_PROOFS~141
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71a647b10a66a7652ed94506db935870bf65b491;p=helm.git

Syntax of <attributes>...</attributes> improved to allow arguments for
classes.
---

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: -->