From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- clib/orderedType.ml | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 clib/orderedType.ml (limited to 'clib/orderedType.ml') diff --git a/clib/orderedType.ml b/clib/orderedType.ml new file mode 100644 index 00000000..922eb76a --- /dev/null +++ b/clib/orderedType.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* t -> int +end + +module Pair (M:S) (N:S) = struct + type t = M.t * N.t + + let compare (a,b) (a',b') = + let i = M.compare a a' in + if Int.equal i 0 then N.compare b b' + else i +end + +module UnorderedPair (M:S) = struct + type t = M.t * M.t + + let reorder (a,b as p) = + if M.compare a b <= 0 then p else (b,a) + + let compare p p' = + let p = reorder p and p' = reorder p' in + let module P = Pair(M)(M) in P.compare p p' +end -- cgit v1.2.3