moved list_uniq to the extlib

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index 75d0f67e0e2b12985769b7dc4c59fcfe5bd12a36..e3c7041ddadd927d4f6b86fe0b0e4e3d0c42b306 100644 (file)
--- 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 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

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index 0c2063095d7dc9ab29a7fb0d360081cc1955c0e7..1f72dbddd4332da4bbea16534333e22985501ea3 100644 (file)
--- 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 51268acef0c8084216a7107346308b23813f3416..77a7d7b6f633c64233404f672ea9db4412946ffb 100644 (file)
--- 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 5a73c099bee3866cd1d8294c3a6e8e0e13c5c573..40f91235a5a9e9ac82ae6d7e9c66f5253034a8f4 100644 (file)
--- 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);