- May 24, 2022
-
-
Ralf Jung authored
-
-
- May 18, 2022
-
-
Ralf Jung authored
Make Hoare triple tex macro compatible with e.g. array environment See merge request iris/iris!797
-
- May 17, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
Add testcase for #461 See merge request iris/iris!798
-
- May 16, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Jonas Kastberg authored
-
Jonas Kastberg authored
-
Ralf Jung authored
-
- May 13, 2022
-
-
Ralf Jung authored
-
Jonas Kastberg authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
make affinely_True_emp more useful, and make absorbingly lemmas consistent See merge request iris/iris!796
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. See merge request iris/iris!793
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Also fix some places where we break the seal.
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
port to dom D type being implicit See merge request iris/iris!795
-
Ralf Jung authored
-
- May 11, 2022
-
-
Ralf Jung authored
Updated suggested emacs indendation configuration See merge request iris/iris!776
-
-
- May 09, 2022
-
-
Ralf Jung authored
add big_sepS_insert_2' and big_sepS_union_2 See merge request iris/iris!787
-
-
Ralf Jung authored
-
- May 08, 2022
-
-
Ralf Jung authored
-
- May 07, 2022
-
-
Ralf Jung authored
-
- May 06, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
Pick universes for [bi_tforall] and [bi_texist]. See merge request iris/iris!781
-
This requires the [fixpoint] version of [tele_arg].
-