| Name of string
| Anonymous
+type object_flavour =
+ [ `Definition
+ | `Fact
+ | `Lemma
+ | `Remark
+ | `Theorem
+ | `Variant
+ ]
+
type object_class =
[ `Coercion
| `Elim of sort (** elimination principle; if sort is Type, the universe is
type attribute =
[ `Class of object_class
+ | `Flavour of object_flavour
| `Generated
]