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.ml | |
| 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.ml')
| -rw-r--r-- | interp/notation.ml | 6 |
1 files changed, 6 insertions, 0 deletions
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 |