diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 15:38:32 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 15:38:32 -0500 |
| commit | 601c2aeaab47edf2cc8dc705e712fb89b96f5ff9 (patch) | |
| tree | b57385e30eb54e00239a24cb63d4f7943506e438 /src/Util/SideConditions/CorePackages.v | |
| parent | 39c12e5c7225fd30dbe2364b208f4764f1fdb457 (diff) | |
Allow pre-unfolding of autosolve things
Diffstat (limited to 'src/Util/SideConditions/CorePackages.v')
| -rw-r--r-- | src/Util/SideConditions/CorePackages.v | 5 |
1 files changed, 5 insertions, 0 deletions
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 (). |