diff options
| author | Jason Gross | 2018-11-27 21:03:57 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:01:17 -0500 |
| commit | f7992de2dc4ce0091197b9476779fc120a2fd9ec (patch) | |
| tree | 236d3a9e0b2e357b893653d97b41303cb8d5529c /vernac | |
| parent | 26ef08ab681661c03c8bffa88d7bec949d692f58 (diff) | |
Factor out common code in numeral/string notations
As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 6 | ||||
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/himsg.mli | 2 |
3 files changed, 6 insertions, 8 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index b238c96913..e1496e58d7 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -64,10 +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_or_string_notation_error "numeral" ctx sigma te) - | Notation.StringNotationError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "string" ctx sigma te) + | Notation.PrimTokenNotationError(kind,ctx,sigma,te) -> + wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind 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 bf3bd70f09..436f7dce37 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1326,12 +1326,12 @@ let explain_reduction_tactic_error = function spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' (Evd.from_env env') e -let explain_numeral_or_string_notation_error numeral_or_string env sigma = function +let explain_prim_token_notation_error kind env sigma = function | Notation.UnexpectedTerm c -> (strbrk "Unexpected term " ++ pr_constr_env env sigma c ++ - strbrk (" while parsing a "^numeral_or_string^" notation.")) + strbrk (" while parsing a "^kind^" notation.")) | Notation.UnexpectedNonOptionTerm c -> (strbrk "Unexpected non-option term " ++ pr_constr_env env sigma c ++ - strbrk (" while parsing a "^numeral_or_string^" notation.")) + strbrk (" while parsing a "^kind^" notation.")) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index ecb69bef1e..bab66b2af4 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -47,4 +47,4 @@ 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_or_string_notation_error : string -> env -> Evd.evar_map -> Notation.numeral_or_string_notation_error -> Pp.t +val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t |