val nonrec_kbo: Cic.term -> Cic.term -> comparison
+val string_of_equality:
+ ?env:Inference.environment -> Inference.equality -> string
+
val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison
val names_of_context: Cic.context -> (Cic.name option) list