X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fdtd%2Fcic.dtd;h=a4068754f451274c9aa5b2388ad583c539964f58;hb=23886971f037b00a358d9b422aa0b3b40a75dc10;hp=164945d2a0b238ed1fd51f5ff9708c35d1504a5f;hpb=d59f9b0745bd3e2da8a5fbcd87158f0b5544c6e1;p=helm.git

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 164945d2a..a4068754f 100644
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -43,8 +43,9 @@
 
 <!ELEMENT Variable (body?,type)>
 <!ATTLIST Variable
-          name CDATA #REQUIRED
-          id   ID    #REQUIRED>
+          name   CDATA #REQUIRED
+          params CDATA #REQUIRED
+          id     ID    #REQUIRED>
 
 <!ELEMENT Sequent %sequent;>
 <!ATTLIST Sequent
@@ -196,7 +197,7 @@
 
 <!-- Explicit named substitutions: -->
 
-<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)>
+<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)>
 <!ATTLIST instantiate
           id ID #IMPLIED>