Djot_kernel.OrderedType
type 'x coq_Compare =
| LT
| EQ
| GT
module type OrderedType = sig ... end
module OrderedTypeFacts (O : OrderedType) : sig ... end
module KeyOrderedType (O : OrderedType) : sig ... end