diff options
Diffstat (limited to 'topbin')
| -rw-r--r-- | topbin/coqtop_byte_bin.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index aaabd90370..604c6e251a 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/topbin/coqtop_byte_bin.ml @@ -8,6 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* We register this handler for lower-level toplevel loading code *) +let _ = CErrors.register_handler (function + | Symtable.Error e -> + Pp.str (Format.asprintf "%a" Symtable.report_error e) + | _ -> + raise CErrors.Unhandled + ) + let drop_setup () = begin try (* Enable rectypes in the toplevel if it has the directive #rectypes *) @@ -23,7 +31,6 @@ let drop_setup () = { load_obj = (fun f -> if not (Topdirs.load_file ppf f) then CErrors.user_err Pp.(str ("Could not load plugin "^f)) ); - use_file = Topdirs.dir_use ppf; add_dir = Topdirs.dir_directory; ml_loop = (fun () -> Toploop.loop ppf); }) |