diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7e301ba0e..ec390683f 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -182,13 +182,6 @@ let print_location_in_file s inlibrary fname loc = (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) -let print_command_location ib dloc = - match dloc with - | Some (bp,ep) -> - (str"Error during interpretation of command:" ++ fnl () ++ - str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ()) - | None -> (mt ()) - let valid_loc dloc loc = loc <> Loc.ghost & match dloc with |