- Oct 21, 2023
-
-
Robbert Krebbers authored
-
Ralf Jung authored -
Ralf Jung authored
make Z_local_update statement more intuitive See merge request iris/iris!1010
-
Ralf Jung authored
-
-
Ralf Jung authored
add back the ability to skip reference file checks on some Coq versions See merge request iris/iris!1011
-
- Oct 20, 2023
- Oct 17, 2023
-
-
Ralf Jung authored
-
- Oct 16, 2023
-
-
Ralf Jung authored
generalize iso_cmra_mixin_restrict to a lemma that can also restrict the domain See merge request iris/iris!970
-
Ralf Jung authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
have solve_proper exploit OfeDiscrete and LeibnizEquiv See merge request iris/iris!968
-
Ralf Jung authored
-
Ralf Jung authored
-
- Oct 15, 2023
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Fix local notations in `bi/embedding`. See merge request iris/iris!1006
-
Robbert Krebbers authored
Add lemmas for using `IdFree` at the logic level. See merge request iris/iris!1005
-
Robbert Krebbers authored
-
Robbert Krebbers authored
better errors on WP mask mismatches See merge request iris/iris!1001
-
- Oct 14, 2023
-
-
Robbert Krebbers authored
-
- Oct 13, 2023
- Oct 12, 2023
-
-
Ralf Jung authored
-
- Oct 11, 2023
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Release 4.1.0 See merge request iris/iris!1003
-
Ike Mulder authored
-
Johannes Hostert authored
-
- Oct 09, 2023
-
-
Ralf Jung authored
Streamline "inversion" lemmas for `dist` on `list` See merge request iris/iris!1002
-
-
- Oct 08, 2023
-
-
Robbert Krebbers authored
-
- Oct 07, 2023
-
-
Ralf Jung authored
-
- Oct 06, 2023
-
-
Ralf Jung authored
Lemmas and instances for `∪` on `gmap`. See merge request iris/iris!998
-
Robbert Krebbers authored
`Inj`/`Forall2` results for `list`/`option` similar to std++. See merge request iris/iris!999
-
