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
| [ "value", "theorem"] -> Obj_flavour `Theorem
| [ "value", "variant"] -> Obj_flavour `Variant
+ | [ "value", "axiom"] -> Obj_flavour `Axiom
| _ -> attribute_error ())
| "class" ->
let class_modifiers = pop_class_modifiers ctxt in
push ctxt
(match pop_tag_attrs ctxt with
- | ["value", "coercion"] -> Obj_class `Coercion
+ | ["value", "coercion"] -> Obj_class (`Coercion 0)
+ | ("value", "coercion")::["arity",n]
+ | ("arity",n)::["value", "coercion"] ->
+ let arity = try int_of_string n with Failure _ ->
+ parse_error "\"arity\" must be an integer"
+ in
+ Obj_class (`Coercion arity)
| ["value", "elim"] ->
(match class_modifiers with
| [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
(function
| Obj_field name ->
(match Str.split (Str.regexp " ") name with
- | [name] -> name, false
- | [name;"coercion"] -> name,true
+ | [name] -> name, false, 0
+ | [name;"coercion"] -> name,true,0
+ | [name;"coercion"; n] ->
+ let n =
+ try int_of_string n
+ with Failure _ ->
+ parse_error "int expected after \"coercion\""
+ in
+ name,true,n
| _ ->
parse_error
"wrong \"field\"'s name attribute")
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))