A bit more reorganization of autosolve

This lets other files import evar_package without having to be rebuilt every time a new package alias is added to Autosolve

2 files changed, 18 insertions, 14 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 86bd21860..7bc47def3 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -1,21 +1,9 @@
-Import EqNotations.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.SideConditions.CorePackages.
 
 Definition vm_decide_package (P : Prop) := P.
 Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P.
 Definition vm_compute_reflexivity_package (P : Prop) := P.
-Record evar_package {T} (v : T) :=
-  { val : T;
-    evar_package_pf : val = v }.
-Arguments val {T v} _.
-Arguments evar_package_pf {T v} _.
-Record evard_package {s d} (v : s) :=
-  { vald : d;
-    evard_package_pfT : s = d;
-    evard_package_pf : vald = rew evard_package_pfT in v }.
-Arguments vald {s d v} _.
-Arguments evard_package_pfT {s d v} _.
-Arguments evard_package_pf {s d v} _.
 Inductive cast_bias := LHS | RHS.
 Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
   @evar_package T v.
@@ -50,4 +38,4 @@ Module Internal.
     end.
 End Internal.
 
-Ltac autosolve := Internal.autosolve.
+Ltac autosolve ::= Internal.autosolve.
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v
new file mode 100644
index 000000000..19612df0a
--- /dev/null
+++ b/src/Util/SideConditions/CorePackages.v
@@ -0,0 +1,16 @@
+Import EqNotations.
+
+Record evar_package {T} (v : T) :=
+  { val : T;
+    evar_package_pf : val = v }.
+Arguments val {T v} _.
+Arguments evar_package_pf {T v} _.
+Record evard_package {s d} (v : s) :=
+  { vald : d;
+    evard_package_pfT : s = d;
+    evard_package_pf : vald = rew evard_package_pfT in v }.
+Arguments vald {s d v} _.
+Arguments evard_package_pfT {s d v} _.
+Arguments evard_package_pf {s d v} _.
+
+Ltac autosolve else_tac := else_tac ().