Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 9 insertions, 9 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b2fd0c1d7..1655ffb8a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1292,7 +1292,7 @@ let load_file handler f =
   try
     Minilib.log "Loading file starts";
     let is_f = CUnix.same_file f in
-      if not (Util.list_fold_left_i
+      if not (Util.List.fold_left_i
 		(fun i found x -> if found then found else
                    let {analyzed_view=av} = x in
                      (match av#filename with
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index d09adb474..5a72669b8 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -55,7 +55,7 @@ class command_window coqtop =
   let remove_cb () =
     let index = notebook#current_page in
     let () = notebook#remove_page index in
-    views := Util.list_filter_i (fun i x -> i <> index) !views
+    views := Util.List.filter_i (fun i x -> i <> index) !views
   in
   let _ =
     toolbar#insert_button
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index df3d8df05..c75b371fe 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -16,14 +16,14 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#append_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Util.List.chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 (* XXX - Temporary hack to compile with archaic lablgtk
   method insert_term ?(build=default_build) ?pos (term:'a) =
     let tab_label,menu_label,page = build term in
     let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Util.List.chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -32,26 +32,26 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#prepend_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Util.List.chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
   method set_term (term:'a) =
     let tab_label,menu_label,page = make_page term in
     let real_pos = super#current_page in
-      term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+      term_list <- Util.List.map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
       super#set_page ?tab_label ?menu_label page
 
   method get_nth_term i =
     List.nth term_list i
 
   method term_num p =
-    Util.list_index0 p term_list
+    Util.List.index0 p term_list
 
   method pages = term_list
 
   method remove_page index =
-    term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+    term_list <- Util.List.filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
   method current_term =
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index af9dcba3a..5da0eeceb 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -100,7 +100,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         proof#buffer#insert (goal_str i goals_cnt);
         proof#buffer#insert (g ^ "\n")
       in
-      let () = Util.list_fold_left_i fold_goal 2 () rem_goals in
+      let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
 
       ignore(proof#buffer#place_cursor
                ~where:(proof#buffer#end_iter#backward_to_tag_toggle