type object_flavour =
[ `Definition
+ | `MutualDefinition
| `Fact
| `Lemma
| `Remark
the record fields names and if they are coercions and
then the coercion arity *)
| `Projection (** record projection *)
+ | `InversionPrinciple (** inversion principle *)
]
type attribute =