]> matita.cs.unibo.it Git - helm.git/commitdiff
extlib list_uniq instead of local copy
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 19 Apr 2008 16:27:57 +0000 (16:27 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 19 Apr 2008 16:27:57 +0000 (16:27 +0000)
helm/software/components/cic_proof_checking/cicUnivUtils.ml

index d61545ff66bea18a4dd2d997c1f67d2d2010d973..948b26ff0bf62e372648f8ab175112cd0b455d9a 100644 (file)
@@ -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 *)