diff options
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 (). |