From e960cd8dac76829f3a48167e70a23c65d8dd797f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 16 Apr 2010 14:13:00 +0000
Subject: Util: remove list_split_at which is a clone of list_chop

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/typed_notebook.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index 39e8155d3f..cadb5941e4 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -18,14 +18,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_split_at 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_split_at real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -34,7 +34,7 @@ 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_split_at real_pos term_list in
+    let lower,higher = Util.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
-- 
cgit v1.2.3