- Jan 24, 2022
-
-
Robbert Krebbers authored
Stop `iAssumption` from unifying evar premises with `False` See merge request iris/iris!772
-
-
- Jan 23, 2022
-
-
Ralf Jung authored -
Tej Chajed authored
-
Ralf Jung authored
Iris 3.6.0 release notes See merge request iris/iris!777
-
-
- Jan 17, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
unstage mono_list algebra See merge request iris/iris!761
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
mono_nat algebra: add dfrac support and notation See merge request iris/iris!759
-
Ralf Jung authored
don't make frame_fractional an instance Closes #351 See merge request iris/iris!739
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
remove auth_frac_op lemmas See merge request iris/iris!774
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 15, 2022
-
-
Ralf Jung authored
rename the new dfrac_agree update lemmas for consistency See merge request iris/iris!769
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jan 14, 2022
-
-
Robbert Krebbers authored
Fix bi_rewrite_relation hint priority See merge request iris/iris!773
-
-
- Jan 13, 2022
-
-
Robbert Krebbers authored
-
- Jan 12, 2022
-
-
Robbert Krebbers authored
-
- Jan 11, 2022
-
-
Robbert Krebbers authored
Formulate `is_closed_expr` in terms of `gset`s. See merge request iris/iris!707
-
Dan Frumin authored -
Robbert Krebbers authored
-
Dan Frumin authored
And prove some additional lemmas.
-
- Dec 30, 2021
-
-
Ralf Jung authored
Fix name, `Later_inj` -> `Next_inj`. See merge request iris/iris!770
-
-
- Dec 17, 2021
-
-
-
Ralf Jung authored
These type annotations are no longer needed once we have a bidirectionality hint on tele_app.
-
Ralf Jung authored
drop support for Coq 8.12 See merge request iris/iris!763
-
Ralf Jung authored
-
Ralf Jung authored
equip frac_agree with support for dfrac See merge request iris/iris!766
-
