Allow pre-unfolding of autosolve things

2 files changed, 29 insertions, 27 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 90c317742..3873ff7b9 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -13,30 +13,27 @@ Notation vm_compute_evar_package := vm_compute_evar_package_vm_small.
 Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v.
 Definition cast_evar_package {s} (v : s) d := @evard_package s d v.
 
-Module Internal.
-  Ltac autosolve else_tac :=
-    lazymatch goal with
-    | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
-    | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
-    | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
-    | [ |- vm_compute_evar_package_vm_small ?v ]
-      => let v' := (eval vm_compute in v) in
-         (exists v'); abstract vm_cast_no_check (eq_refl v')
-    | [ |- vm_compute_evar_package_vm_large ?v ]
-      => let v' := (eval vm_compute in v) in
-         (exists v'); abstract vm_cast_no_check (eq_refl v)
-    | [ |- vm_cast_evar_package ?v ?d ]
-      => unshelve eexists (v <: d);
-         [ vm_compute; reflexivity
-         | cbv beta;
-           let lhs := lazymatch goal with |- ?lhs = _ => lhs end in
-           abstract exact_no_check (eq_refl lhs) ]
-    | [ |- cast_evar_package (s:=?s) ?v ?d ]
-      => exact (@Build_evard_package
-                  s d v
-                  v eq_refl eq_refl)
-    | _ => else_tac ()
-    end.
-End Internal.
-
-Ltac autosolve ::= Internal.autosolve.
+Ltac autosolve else_tac :=
+  CorePackages.preautosolve ();
+  lazymatch goal with
+  | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
+  | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
+  | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
+  | [ |- vm_compute_evar_package_vm_small ?v ]
+    => let v' := (eval vm_compute in v) in
+       (exists v'); abstract vm_cast_no_check (eq_refl v')
+  | [ |- vm_compute_evar_package_vm_large ?v ]
+    => let v' := (eval vm_compute in v) in
+       (exists v'); abstract vm_cast_no_check (eq_refl v)
+  | [ |- vm_cast_evar_package ?v ?d ]
+    => unshelve eexists (v <: d);
+       [ vm_compute; reflexivity
+       | cbv beta;
+         let lhs := lazymatch goal with |- ?lhs = _ => lhs end in
+         abstract exact_no_check (eq_refl lhs) ]
+  | [ |- cast_evar_package (s:=?s) ?v ?d ]
+    => exact (@Build_evard_package
+                s d v
+                v eq_refl eq_refl)
+  | _ => CorePackages.autosolve else_tac
+  end.
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v
index fbe8df7cc..ad0756f89 100644
--- a/src/Util/SideConditions/CorePackages.v
+++ b/src/Util/SideConditions/CorePackages.v
@@ -2,6 +2,8 @@ Import EqNotations.
 
 Local Set Primitive Projections.
 
+Create HintDb autosolve discriminated.
+
 Definition raw_evar_package (T : Type) := T.
 
 Record evar_Prop_package {T} (P : T -> Prop) :=
@@ -39,4 +41,7 @@ Definition evard_package_pf {s d v} (pkg : @evard_package s d v)
   : val pkg = rew (evard_package_pfT pkg) in v
   := Eval cbv [proj1_sig evar_package_pf] in proj2_sig (evar_package_pf pkg).
 
+Ltac preautosolve _ :=
+  repeat autounfold with autosolve in *.
+
 Ltac autosolve else_tac := else_tac ().