Add autosolve admit package

2 files changed, 14 insertions, 1 deletions

diff --git a/src/Util/SideConditions/AdmitPackage.v b/src/Util/SideConditions/AdmitPackage.v
new file mode 100644
index 000000000..c25e82aba
--- /dev/null
+++ b/src/Util/SideConditions/AdmitPackage.v
@@ -0,0 +1,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.
diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 51c13647c..7d2f1a9c7 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -1,15 +1,17 @@
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.SideConditions.CorePackages.
+Require Import Crypto.Util.SideConditions.AdmitPackage.
 Require Import Crypto.Util.SideConditions.ReductionPackages.
 Require Import Crypto.Util.SideConditions.RingPackage.
 
 Ltac autosolve_gen autosolve_tac else_tac :=
   CorePackages.preautosolve ();
   CorePackages.Internal.autosolve ltac:(fun _ =>
+  AdmitPackage.autosolve ltac:(fun _ =>
   ReductionPackages.autosolve autosolve_tac ltac:(fun _ =>
   RingPackage.autosolve ltac:(fun _ =>
   CorePackages.autosolve else_tac
-                                       ))).
+                                       )))).
 
 Ltac autosolve else_tac :=
   autosolve_gen autosolve else_tac.