diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 74ed231d1..7e301ba0e 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -291,6 +291,12 @@ let print_toplevel_error exc = (print_highlight_location top_buffer loc, ie) else ((mt ()) (* print_command_location top_buffer dloc *), ie) + | Compat.Exc_located (loc, ie) -> + let loc = Compat.to_coqloc loc in + if valid_buffer_loc top_buffer dloc loc then + (print_highlight_location top_buffer loc, ie) + else + ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) | _ -> |