diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/wg_Command.ml | 2 | ||||
| -rw-r--r-- | ide/wg_Notebook.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 5a72669b82..2e4ce364de 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.filteri (fun i x -> i <> index) !views in let _ = toolbar#insert_button diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index c75b371fed..7a4ddc010f 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -51,7 +51,7 @@ object(self) 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.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list; super#remove_page index method current_term = |