(string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
| Meta_subst of Cic.annterm option
| Obj_class of Cic.object_class
+ | Obj_flavour of Cic.object_flavour
| Obj_field of string (* field name *)
| Obj_generated
| Tag of string * (string * string) list (* tag name, attributes *)
sprintf "Inductive_type %s (id=%s)" name id
| Meta_subst _ -> "Meta_subst"
| Obj_class _ -> "Obj_class"
+ | Obj_flavour _ -> "Obj_flavour"
| Obj_field name -> "Obj_field " ^ name
| Obj_generated -> "Obj_generated"
| Tag (tag, _) -> "Tag " ^ tag)
| "attributes" ->
let rec aux acc = function (* retrieve object attributes *)
| Obj_class c :: tl -> aux (`Class c :: acc) tl
+ | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
| Obj_generated :: tl -> aux (`Generated :: acc) tl
| tl -> acc, tl
in
(match pop_tag_attrs ctxt with
| ["name", name] -> Obj_field name
| _ -> attribute_error ())
+ | "flavour" ->
+ push ctxt
+ (match pop_tag_attrs ctxt with
+ | [ "value", "definition"] -> Obj_flavour `Definition
+ | [ "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
+ | _ -> attribute_error ())
| "class" ->
let class_modifiers = pop_class_modifiers ctxt in
push ctxt