From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 7 Jun 2005 17:20:33 +0000 (+0000)
Subject: added object attributes
X-Git-Tag: PRE_INDEX_1~51
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb379a463ec772df8855310fc9bf7276ea5f3f3d;p=helm.git

added object attributes
---

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 97e6cd6b1..840f797f6 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,11 @@
           no  NMTOKEN #REQUIRED
           id  ID      #REQUIRED>
 
+<!ELEMENT attributes EMPTY>
+<!ATTLIST attributes
+          class (coercion|elimProp|elimCProp|elimSet|elimType|record|projection) #IMPLIED
+          generated   (true|false)  #IMPLIED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -139,7 +144,8 @@
 
 <!ELEMENT IMPLICIT EMPTY>
 <!ATTLIST IMPLICIT
-          id ID #REQUIRED>
+          id ID #REQUIRED
+	  annotation (closed|type|hole) #IMPLIED>
 
 <!ELEMENT CONST EMPTY>
 <!ATTLIST CONST