diff options
| author | Jason Gross | 2018-09-19 09:32:15 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-09-19 18:43:02 -0400 |
| commit | 4888eb7ea720eaa34af8df2769fa300f1ea37173 (patch) | |
| tree | c0776bc016413ba89d226d8fd9828a2d6c47be5e /interp/notation.mli | |
| parent | e39c84ff2dc20ce059ee6198e142ca076de8c6cb (diff) | |
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.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 6 |
1 files changed, 6 insertions, 0 deletions
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 |