From 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 3 Mar 2019 16:49:30 +0100
Subject: [error] Remove special error printing pre-processing

We remove the special error printing pre-processing in favor of just
calling the standard printers.

Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.

After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.

This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
---
 dev/base_include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index b30bbaa3fa..4841db8953 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open ExplainErr
 open Class
 open ComDefinition
 open Indschemes
-- 
cgit v1.2.3