- Oct 24, 2023
-
-
Ralf Jung authoredFollowup for iris/iris!1011 See merge request iris/iris!1014
-
Ralf Jung authored
-
- Oct 23, 2023
-
-
Pierre Roux authored
Now works with Coq master which prints version 8.19+alpha
-
- 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
-
-
-
- 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
-
