Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • robbert/cmra_valid_elim
  • ralf/separable
  • robbert/mono_Z
  • ralf/Z
  • ralf/bi-persistently-emp
  • ralf/mono_Z
  • ci/robbert/big_op_binder
  • robbert/no_native_compute
  • simon/parametric-index
  • ci/robbert/set_solver_eauto
  • ralf/make
  • ci/msammler/nb_state
  • robbert/add_sub
  • ci/general-contractive
  • ralf/has-lc
  • robbert/has_lc_if
  • robbert/bi_cofe
  • robbert/bi_wand_notation
  • robbert/level
  • 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
No longer break now_True abstraction.
Robbert Krebbers authored 
And make it Typeclasses Opaque to ensure that we indeed do not do
so using the proof mode.
51b15fdc
History
user avatar 51b15fdc
History
Name Last commit Last update