+ 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
+ let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in