blob: 154f1d2ae69acd57979c0ed2e7cdf05808c582df (
plain)
1
2
3
4
5
6
7
8
|
Require Export Crypto.Util.FixCoqMistakes.
Require Export Crypto.Util.Tactics.UniquePose.
Ltac specialize_all_ways :=
repeat match goal with
| [ H : ?A, H' : forall a : ?A, _ |- _ ]
=> unique pose proof (H' H)
end.
|