]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicPushParser.ml
fixed Makefile
[helm.git] / helm / ocaml / cic / cicPushParser.ml
index 31ded7ef22d74efab484affc82cd92f7dde82daf..c6f56dad9368beef7cc4d061e2464458bb2d4553 100644 (file)
@@ -35,7 +35,6 @@ open Printf
    <!ELEMENT Def %term;>
    <!ELEMENT Hidden EMPTY>
    <!ELEMENT Goal %term;>
-   <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern* )>
 *)
 
 module CicParser =
@@ -639,12 +638,13 @@ let parse uri filename =
   let xml_parser = P.create_parser callbacks in
   ctxt.xml_parser <- Some xml_parser;
   try
-    P.parse xml_parser (`File filename);
+    P.parse xml_parser (`Gzip_file filename);
 (*    debug_print (string_of_stack stack);*)
     List.hd ctxt.stack
   with
   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
+  | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
   | Parser_failure _
   | Getter_failure _ as exn ->
       raise exn