blob: fe8a05630198889af610cc727f4a12b8b9a8e7fc (
plain)
1
2
3
4
5
6
7
8
9
|
(** A tactic that executes immediately (during expression evaluation / constr-construction) and fails. Ideally we can eventually give it a nicer error message. COQBUG(3913) *)
Ltac constr_fail :=
let __ := match goal with _ => fail 1 "Constr construction failed. Please look at the message log (*coq*, or run your tactic again inside Fail or try) to see more details" end in
().
Ltac constr_fail_with msg_tac :=
let __ := match goal with _ => msg_tac () end in
constr_fail.
|
