blob: 840d3a592e556a27ed68d120185ea703b48f9d75 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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.
Ltac autosolve_gen autosolve_tac ring_intros_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_gen_intros ring_intros_tac ltac:(fun _ =>
CorePackages.autosolve else_tac
))))).
Ltac autosolve_gen_intros ring_intros_tac else_tac :=
autosolve_gen ltac:(autosolve_gen_intros ring_intros_tac) ring_intros_tac else_tac.
Ltac autosolve else_tac := autosolve_gen_intros default_ring_intros_tac else_tac.
|
