fixed a TODO comment (MUTCASE _is_ implemented)

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 9a0566ec2e6048d3801b60a1f33dffda65b8db11..c6f56dad9368beef7cc4d061e2464458bb2d4553 100644 (file)
--- 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 =