Allow pre-unfolding of autosolve things

1 files changed, 24 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.