diff options
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 |