Proofs.MXmodule TO : sig ... endmodule IsTO : sig ... endmodule OrderTac : sig ... endval eq_dec : Eqtype.Equality.sort -> Eqtype.Equality.sort -> boolval lt_dec : Eqtype.Equality.sort -> Eqtype.Equality.sort -> boolval eqb : Eqtype.Equality.sort -> Eqtype.Equality.sort -> bool