Skip to content
GitLab
Explore
Sign in
Iris
Iris
Repository
iris
iris_heap_lang
proofmode.v
Find file
Blame
History
Permalink
Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply`
· a361b173
Robbert Krebbers
authored
Nov 12, 2020
that performs `wp_pure` in small steps until the lemma matches the goal.
a361b173