diff options
Diffstat (limited to 'debugger/events.mli')
| -rw-r--r-- | debugger/events.mli | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/debugger/events.mli b/debugger/events.mli index 43fa8600b1..d71f81286a 100644 --- a/debugger/events.mli +++ b/debugger/events.mli @@ -28,16 +28,3 @@ val current_point : unit -> string * int val current_event_is_before : unit -> bool -(** Finding events. **) - -(* List the events in `module'. *) -(* ### module -> event_list *) -val events_in_module : string -> debug_event list - -(* First event after the given position. *) -(* --- Raise `Not_found' if no such event. *) -val event_after_pos : string -> int -> debug_event - -(* Nearest event from given position. *) -(* --- Raise `Not_found' if no such event. *) -val event_near_pos : string -> int -> debug_event |