Add ModInv autosolver

1 files changed, 3 insertions, 1 deletions

diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v
index 7d2f1a9c7..9f8eb61de 100644
--- a/src/Util/SideConditions/Autosolve.v
+++ b/src/Util/SideConditions/Autosolve.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.SideConditions.CorePackages.
 Require Import Crypto.Util.SideConditions.AdmitPackage.
+Require Import Crypto.Util.SideConditions.ModInvPackage.
 Require Import Crypto.Util.SideConditions.ReductionPackages.
 Require Import Crypto.Util.SideConditions.RingPackage.
 
@@ -8,10 +9,11 @@ Ltac autosolve_gen autosolve_tac else_tac :=
   CorePackages.preautosolve ();
   CorePackages.Internal.autosolve ltac:(fun _ =>
   AdmitPackage.autosolve ltac:(fun _ =>
+  ModInvPackage.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.