diff options
Diffstat (limited to 'ide/wg_Notebook.mli')
| -rw-r--r-- | ide/wg_Notebook.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli index a424fc0295..df64743871 100644 --- a/ide/wg_Notebook.mli +++ b/ide/wg_Notebook.mli @@ -16,7 +16,7 @@ object method prepend_term : 'a -> int method set_term : 'a -> unit method get_nth_term : int -> 'a - method term_num : 'a -> int + method term_num : ('a -> 'a -> bool) -> 'a -> int method pages : 'a list method remove_page : int -> unit method current_term : 'a |