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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 10 | ||||
| -rw-r--r-- | vernac/himsg.mli | 2 |
3 files changed, 14 insertions, 0 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 504e7095b0..7cf4e64805 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -64,6 +64,8 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + | Notation.NumeralNotationError(ctx,sigma,te) -> + wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4650cfd92..e7b2a0e8a6 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1315,3 +1315,13 @@ let explain_reduction_tactic_error = function quote (pr_goal_concl_style_env env sigma c) ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' (Evd.from_env env') e + +let explain_numeral_notation_error env sigma = function + | Notation.UnexpectedTerm c -> + (strbrk "Unexpected term " ++ + pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") + | Notation.UnexpectedNonOptionTerm c -> + (strbrk "Unexpected non-option term " ++ + pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 91caddcf13..02b3c45501 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -46,3 +46,5 @@ val explain_module_internalization_error : val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error + +val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t |