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.
---
 interp/notation.ml  | 6 ++++++
 interp/notation.mli | 6 ++++++
 2 files changed, 12 insertions(+)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index 8cb423051a..25772d8fe4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -389,6 +389,12 @@ let prim_token_uninterpreters =
 
 (*******************************************************)
 (* Numeral notation interpretation                     *)
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
 type numnot_option =
   | Nop
   | Warning of raw_natural_number
diff --git a/interp/notation.mli b/interp/notation.mli
index 7f20a2ef1f..33e275d925 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -104,6 +104,12 @@ val register_string_interpretation :
 
 (** * Numeral notation *)
 
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
 type numnot_option =
   | Nop
   | Warning of raw_natural_number
-- 
cgit v1.2.3