From efc3d154e69c0fb18215901f5c4de3a73ebc2fb5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 19 Apr 2008 16:27:57 +0000 Subject: [PATCH] extlib list_uniq instead of local copy --- .../components/cic_proof_checking/cicUnivUtils.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicUnivUtils.ml b/helm/software/components/cic_proof_checking/cicUnivUtils.ml index d61545ff6..948b26ff0 100644 --- a/helm/software/components/cic_proof_checking/cicUnivUtils.ml +++ b/helm/software/components/cic_proof_checking/cicUnivUtils.ml @@ -123,14 +123,8 @@ let universes_of_obj uri t = let o = aux_obj t in List.flatten !results, o -let rec list_uniq = function - | [] -> [] - | h::[] -> [h] - | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl) - | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl - let list_uniq l = - list_uniq (List.fast_sort CicUniv.compare l) + HExtlib.list_uniq (List.fast_sort CicUniv.compare l) let clean_and_fill uri obj ugraph = (* universes of obj fills the universes of the obj with the right uri *) -- 2.39.2