src/Util/Tactics/SpecializeAllWays.v


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.