blob: cee21b6d9b1667c2b133671c89d7f33166ab82f2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Crypto.Util.Tactics.Test.
Require Import Crypto.Util.Tactics.Not.
Require Export Crypto.Util.FixCoqMistakes.
(** Do something with every hypothesis. *)
Ltac do_with_hyp' tac :=
match goal with
| [ H : _ |- _ ] => tac H
end.
(** Do something with any hypothesis, as long as there is only one hypothesis that it works with *)
Ltac do_with_exactly_one_hyp tac :=
match goal with
| [ H : _ |- _ ]
=> test (tac H);
not (idtac; match goal with
| [ H' : _ |- _ ] => tryif constr_eq H H' then fail else tac H'
end);
tac H
end.
|
