diff options
| author | Hugo Herbelin | 2018-12-12 14:07:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-12 14:07:12 +0100 |
| commit | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (patch) | |
| tree | 2e7d4477c2effb1975f7964e2a82a497b28cb3bc /vernac | |
| parent | 84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff) | |
| parent | cac9811632834b0135f4408a32b4a2d391d09a0d (diff) | |
Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 4 | ||||
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/himsg.mli | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index befb4d7ccf..e1496e58d7 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -64,8 +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) + | 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 68d6db75ee..a2b5c8d70a 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_notation_error 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 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 notation.") + strbrk (" while parsing a "^kind^" notation.")) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index db05aaa125..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_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t +val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t |