Djot_kernel.OrdersTac
module MakeOrderTac (O : Orders.EqLtLe) (P : sig ... end) : sig ... end
module OT_to_OrderTac (OT : Orders.OrderedType) : sig ... end