diff options
| author | coqbot-app[bot] | 2020-12-12 18:11:12 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-12 18:11:12 +0000 |
| commit | 81d0936c1ac8a537b5d8083933bce607e55ff28f (patch) | |
| tree | f796eff07f22c308502ad31373b079952a4aed60 /plugins | |
| parent | 233629e8f6e40057a8caf7502047995427740ae8 (diff) | |
| parent | 7615b53cbcee95677996d60eb1c5ecc667559759 (diff) | |
Merge PR #13620: Use a registered printer for tactic coercion failure.
Reviewed-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4c1fe6417e..9abdc2ddbe 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -429,7 +429,15 @@ let pr_value env v = | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) -let error_ltac_variable ?loc id env v s = - CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ +exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string + +let () = CErrors.register_handler begin function +| CoercionError (id, env, v, s) -> + Some (str "Ltac variable " ++ Id.print id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") +| _ -> None +end + +let error_ltac_variable ?loc id env v s = + Loc.raise ?loc (CoercionError (id, env, v, s)) |