X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=8334ccfb62e65aac3e4162731b23d2b3078b5597;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=150fe4ad983f6dab3bad1d117877e6093531b755;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 150fe4ad9..8334ccfb6 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -667,6 +667,7 @@ let end_element ctxt tag =
       push ctxt 
         (match pop_tag_attrs ctxt with
         | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
         | [ "value", "fact"] -> Obj_flavour `Fact
         | [ "value", "lemma"] -> Obj_flavour `Lemma
         | [ "value", "remark"] -> Obj_flavour `Remark
@@ -716,7 +717,8 @@ let end_element ctxt tag =
             in
             Obj_class (`Record fields)
         | ["value", "projection"] -> Obj_class `Projection
-        | _ -> attribute_error ())
+        | ["value", "inversion"] -> Obj_class `InversionPrinciple
+	| _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
@@ -770,7 +772,7 @@ let parse uri filename =
   | Getter_failure _ as exn ->
       raise exn
   | exn ->
-      raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
+      raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn))
 
 (** {2 API implementation} *)