blob: cd96ebcd202e3d9b08da32283ec06516a4284c06 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Export Crypto.Util.FixCoqMistakes.
(** Runs a tactic during expression evaluation phase, returns the constr [I] *)
Ltac run_tactic tac :=
let dummy := match goal with _ => tac () end in
I.
(** Runs a tactic during expression evaluation phase, returning [true] on success and [false] on failure. *)
Ltac is_success_run_tactic tac :=
match goal with
| _ => let dummy := run_tactic tac in
true
| _ => false
end.
(** Runs a tactic during expression evaluation phase; on success,
returns [then_tac ()], otherwise returns [else_tac ()] *)
Ltac constr_tryif_then_else tac then_tac else_tac :=
let success := is_success_run_tactic tac in
lazymatch success with
| true => then_tac ()
| false => else_tac ()
end.
|
