Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.

2 files changed, 15 insertions, 0 deletions

diff --git a/clib/cList.ml b/clib/cList.ml
index 2b627f745..de42886dc 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -122,6 +122,7 @@ sig
   val duplicates : 'a eq -> 'a list -> 'a list
   val uniquize : 'a list -> 'a list
   val sort_uniquize : 'a cmp -> 'a list -> 'a list
+  val min : 'a cmp -> 'a list -> 'a
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
   val combinations : 'a list list -> 'a list list
@@ -971,6 +972,15 @@ let rec uniquize_sorted cmp = function
 let sort_uniquize cmp l =
   uniquize_sorted cmp (List.sort cmp l)
 
+let min cmp l =
+  let rec aux cur = function
+    | [] -> cur
+    | x :: l -> if cmp x cur < 0 then aux x l else aux cur l
+  in
+  match l with
+  | x :: l -> aux x l
+  | [] -> raise Not_found
+
 let rec duplicates cmp = function
   | [] -> []
   | x :: l ->
diff --git a/clib/cList.mli b/clib/cList.mli
index 13e069e94..42fae5ed3 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -376,6 +376,11 @@ sig
   (** Return a sorted version of a list without duplicates
       according to some comparison function. *)
 
+  val min : 'a cmp -> 'a list -> 'a
+  (** Return minimum element according to some comparison function.
+
+      @raise Not_found on an empty list. *)
+
   (** {6 Cartesian product} *)
 
   val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list