(** term-ordering function settable by the user *)
val compare_terms: (Cic.term -> Cic.term -> comparison) ref
-val guarded_simpl: Cic.context -> Cic.term -> Cic.term
+val guarded_simpl: ?debug:bool -> Cic.context -> Cic.term -> Cic.term
type equality_sign = Negative | Positive