diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-25 18:26:55 +0200 |
commit | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (patch) | |
tree | 2649ab1a1480b17b74c7207113d5ae8783f2ee42 /clib/cList.ml | |
parent | 24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff) | |
parent | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (diff) |
Merge PR #7798: Remove hack skipping comparison of algebraic universes in subtyping.
Diffstat (limited to 'clib/cList.ml')
-rw-r--r-- | clib/cList.ml | 10 |
1 files changed, 10 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 -> |