moved list_uniq to the extlib

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e86e4b9a051e33ecfc81ab671b25cc7bd4359c48..8f97b25a9384b9f77f8ec1b7f0aab49893f7526d 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -261,12 +261,6 @@ let obj_file_of_script f =
   let baseuri = baseuri_of_file f in
    obj_file_of_baseuri baseuri
 
-let rec list_uniq = function 
-  | [] -> []
-  | h::[] -> [h]
-  | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
-  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-
 let list_tl_at ?(equality=(==)) e l =
   let rec aux =
     function