From 4888eb7ea720eaa34af8df2769fa300f1ea37173 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:32:15 -0400
Subject: Fix Numeral Notations (2/4 - exceptions, usr_err)

Switch to using exceptions rather than user errors.  This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.

This is commit 2/4 in the fix for #8401.
---
 proofs/logic.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e8ca719932..613581ade7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,7 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
-- 
cgit v1.2.3