Skip to content
Snippets Groups Projects
Select Git revision
  • fossacs
  • core-up
  • upd_plain
  • master default protected
  • robbert/level
  • ci/ralf/frame-frac
  • ralf/f_equiv
  • ralf/f_equiv_ho
  • ralf/sprop
  • robbert/into_ih_Forall
  • ci/hai/siProp
  • robbert/stdpp_mr281
  • ci/ralf/Z_of_nat
  • hai/si_embed
  • ci/ralf/bi-language
  • ralf/coq-bug-13942
  • iris-3.4
  • ci/janno/strict-tc-resolution
  • ralf/vs-mask-adjust
  • ci/robbert/into_fupd
  • fossacs-2025
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
35 results
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply`
Robbert Krebbers authored 
that performs `wp_pure` in small steps until the lemma matches the goal.
a361b173
History
user avatar a361b173
History
Name Last commit Last update
..