Skip to content
Snippets Groups Projects
Select Git revision
  • transitive-closure
  • master default protected
  • simon/parametric-index
  • ci/robbert/set_solver_eauto
  • robbert/rewrite_pure_intro_pat
  • ralf/make
  • ralf/bi-persistently-emp
  • ci/msammler/nb_state
  • robbert/add_sub
  • ci/general-contractive
  • ralf/has-lc
  • robbert/has_lc_if
  • robbert/primproj_unfold
  • robbert/bi_cofe
  • robbert/bi_wand_notation
  • robbert/level
  • ralf/f_equiv
  • ralf/f_equiv_ho
  • ralf/sprop
  • ci/hai/siProp
  • iris-4.0.0
  • iris-3.6.0
  • 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
36 results
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Make it optional that iPoseProofCore performs TC inference lazily.
Robbert Krebbers authored 
For iApply and iRewrite we want that, but for iDestruct and iMod we do not.

This fixes issue #52.
e0789039
History
user avatar e0789039
History
Name Last commit Last update