diff options
| author | Pierre-Marie Pédrot | 2020-12-11 17:55:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 17:55:49 +0100 |
| commit | 7615b53cbcee95677996d60eb1c5ecc667559759 (patch) | |
| tree | 66e90bc5e9e1fbe7c28d3312e4295bf3195b16ff /plugins | |
| parent | c8d2248cbbe2c713605e0c61d7342fad948072da (diff) | |
Use a registered printer for tactic coercion failure.
Otherwise we pay a high cost for printing that might never make it to
the user.
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)) |