src/Util/SideConditions/AdmitPackage.v


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.