From d47a2eaf9d30d56cbc230d8bf8c37054ebeae54f Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 12 May 2005 09:07:27 +0000
Subject: [PATCH] fixed a TODO comment (MUTCASE _is_ implemented)

---
 helm/ocaml/cic/cicPushParser.ml | 1 -
 1 file changed, 1 deletion(-)

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 =
-- 
2.39.2