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.

1 files changed, 1 insertions, 0 deletions

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 *)