val lpo: Cic.term -> Cic.term -> comparison
+val kbo: Cic.term -> Cic.term -> comparison
+
(** term-ordering function settable by the user *)
val compare_terms: (Cic.term -> Cic.term -> comparison) ref
val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
-val debug_print: string -> unit
+val debug_print: string Lazy.t -> unit