From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 12 May 2005 09:07:27 +0000 (+0000)
Subject: fixed a TODO comment (MUTCASE _is_ implemented)
X-Git-Tag: single_binding~83
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=d47a2eaf9d30d56cbc230d8bf8c37054ebeae54f;p=helm.git

fixed a TODO comment (MUTCASE _is_ implemented)
---

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 9a0566ec2..c6f56dad9 100644
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -35,7 +35,6 @@ open Printf
    <!ELEMENT Def %term;>
    <!ELEMENT Hidden EMPTY>
    <!ELEMENT Goal %term;>
-   <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern* )>
 *)
 
 module CicParser =