blob: c25e82abaa59bedd79c86807991b179e63173afe (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Coq.Compat.AdmitAxiom.
Require Import Crypto.Util.SideConditions.CorePackages.
Definition admit_package (P : Prop) := P.
Ltac autosolve else_tac :=
lazymatch goal with
| [ |- admit_package ?P ]
=> change P; admit
| _ => else_tac ()
end.
|