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
type pos = Left | Right
val string_of_pos: pos -> string
+
+val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
+
+val debug_print: string Lazy.t -> unit
+
+val eq_ind_URI: unit -> UriManager.uri
+val eq_ind_r_URI: unit -> UriManager.uri
+val sym_eq_URI: unit -> UriManager.uri
+val eq_XURI: unit -> UriManager.uri
+val trans_eq_URI: unit -> UriManager.uri