1 2 3 4 5 6 7
Require Export Crypto.Util.FixCoqMistakes. (** Do something with every hypothesis. *) Ltac do_with_hyp' tac := match goal with | [ H : _ |- _ ] => tac H end.