aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions/Autosolve.v
blob: 51c13647c96cfa4b34ea9c1359d234053c35ad63 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.SideConditions.CorePackages.
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 _ =>
  ReductionPackages.autosolve autosolve_tac ltac:(fun _ =>
  RingPackage.autosolve ltac:(fun _ =>
  CorePackages.autosolve else_tac
                                       ))).

Ltac autosolve else_tac :=
  autosolve_gen autosolve else_tac.