aboutsummaryrefslogtreecommitdiff
path: root/topbin
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-01-16 19:57:28 +0100
committerEmilio Jesus Gallego Arias2020-01-16 20:00:03 +0100
commitcd7052d68fb1bd56c4c1182a47b180b992abd5e0 (patch)
tree74c29dc6f12c0cc08caa2d0f1348f5707ec1a69d /topbin
parent404a24241e3ff89994aa48524d2b34dcb4773300 (diff)
[mltop] Remove error handling hacks in favor of default methods.
We don't need to handle `Dynlink` errors specially anymore.
Diffstat (limited to 'topbin')
-rw-r--r--topbin/coqtop_byte_bin.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index aaabd90370..85d8a48eda 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 *)