From cd7052d68fb1bd56c4c1182a47b180b992abd5e0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Jan 2020 19:57:28 +0100
Subject: [mltop] Remove error handling hacks in favor of default methods.

We don't need to handle `Dynlink` errors specially anymore.
---
 topbin/coqtop_byte_bin.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'topbin')

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 *)
-- 
cgit v1.2.3