From f8394a52346bf1e6f98e7161e75fb65bd0631391 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Sep 2012 16:17:09 +0000
Subject: 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
---
 ide/wg_Notebook.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'ide/wg_Notebook.ml')

diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index df3d8df05d..c75b371fed 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 =
-- 
cgit v1.2.3