diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 13:45:31 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-10 14:14:28 -0500 |
| commit | 1c38c74bc059f67ec58fc8026eb8ba8742b4913b (patch) | |
| tree | 60ec735ae78c2d23d02bb305d4599d55231ada47 /src/Util/SideConditions/CorePackages.v | |
| parent | d5ac8bc07824d9cf6c7b4698bf38bde85cc84704 (diff) | |
More modularity in autosolve
Diffstat (limited to 'src/Util/SideConditions/CorePackages.v')
| -rw-r--r-- | src/Util/SideConditions/CorePackages.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v index 7af4cc133..c4511c93e 100644 --- a/src/Util/SideConditions/CorePackages.v +++ b/src/Util/SideConditions/CorePackages.v @@ -46,4 +46,14 @@ Definition evard_package_pf {s d v} (pkg : @evard_package s d v) Ltac preautosolve _ := repeat autounfold with autosolve in *. +Module Internal. + Ltac autosolve else_tac := + lazymatch goal with + | [ |- True ] => exact I + | [ |- unit ] => exact tt + | [ |- IDProp ] => exact idProp + | _ => else_tac () + end. +End Internal. + Ltac autosolve else_tac := else_tac (). |