From 0bf96cb668cdd8d14b1c66f8a5241f12c5df9e3a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Sep 2005 14:15:46 +0000
Subject: [PATCH] moved list_uniq to the extlib

---
 helm/matita/matitaDb.ml       | 2 +-
 helm/matita/matitaMisc.ml     | 6 ------
 helm/matita/matitaMisc.mli    | 2 --
 helm/matita/matitacleanLib.ml | 9 ++++-----
 helm/matita/matitadep.ml      | 2 +-
 5 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index 75d0f67e0..e3c7041dd 100644
--- a/helm/matita/matitaDb.ml
+++ b/helm/matita/matitaDb.ml
@@ -148,7 +148,7 @@ let remove_uri uri =
     let l = ref [] in
     HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
     let l = List.sort Pervasives.compare !l in
-    MatitaMisc.list_uniq l
+    HExtlib.list_uniq l
   with
     exn -> raise exn (* no errors should be accepted *)
 
diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e86e4b9a0..8f97b25a9 100644
--- 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
diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index 0c2063095..1f72dbddd 100644
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -56,8 +56,6 @@ val strip_trailing_slash: string -> string
 val normalize_dir: string -> string (** add trailing "/" if missing *)
 val strip_suffix: suffix:string -> string -> string
 
-val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
-
   (** @return tl tail of a list starting at a given element
    * @param eq equality to be used, defaults to physical equality (==)
    * @raise Not_found *)
diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index 51268acef..77a7d7b6f 100644
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -62,7 +62,7 @@ let one_step_depend suri =
                 l := uri :: !l
             | _ -> ());
         let l = List.sort Pervasives.compare !l in
-        MatitaMisc.list_uniq l
+        HExtlib.list_uniq l
       with
         exn -> raise exn (* no errors should be accepted *)
     end
@@ -77,7 +77,7 @@ let safe_buri_of_suri suri =
 let close_uri_list uri_to_remove =
   (* to remove an uri you have to remove the whole script *)
   let buri_to_remove = 
-    MatitaMisc.list_uniq 
+    HExtlib.list_uniq 
       (List.fast_sort Pervasives.compare 
         (List.map safe_buri_of_suri uri_to_remove))
   in
@@ -117,8 +117,7 @@ let close_uri_list uri_to_remove =
     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
   in
   let depend = 
-    MatitaMisc.list_uniq 
-      (List.fast_sort Pervasives.compare depend) 
+    HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
   in
   uri_to_remove, depend
 
@@ -136,7 +135,7 @@ let clean_baseuris ?(verbose=true) buris =
   if debug then
     List.iter debug_prerr buris; 
   let l = close [] buris in
-  let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
+  let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
   debug_prerr "clean_baseuri will remove:";
   if debug then
diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index 5a73c099b..40f91235a 100644
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -107,7 +107,7 @@ let main () =
    (fun file -> 
     let deps = Hashtbl.find_all include_deps file in
     let deps = List.fast_sort Pervasives.compare deps in
-    let deps = MatitaMisc.list_uniq deps in
+    let deps = HExtlib.list_uniq deps in
     let deps = file :: deps in
     let moo = MatitaMisc.obj_file_of_script file in
      Printf.printf "%s: %s\n" moo (String.concat " " deps);
-- 
2.39.2