+ let flavour_pp = function
+ | None -> ""
+ | Some `Definition -> "as definition"
+ | Some `MutualDefinition -> "as mutual"
+ | Some `Fact -> "as fact"
+ | Some `Lemma -> "as lemma"
+ | Some `Remark -> "as remark"
+ | Some `Theorem -> "as theorem"
+ | Some `Variant -> "as variant"
+ | Some `Axiom -> "as axiom"
+ in