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
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))
| 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} *)