- Nov 14, 2023
-
-
Johannes Hostert authored
-
- Nov 11, 2023
-
-
Ralf Jung authoredAdd laws to allow "undiscarding" points-tos See merge request iris/iris!960
-
Ralf Jung authored
Remove needless later in total adequacy. See merge request iris/iris!1018
-
Robbert Krebbers authored
-
- Nov 10, 2023
-
-
Johannes Hostert authored
-
Johannes Hostert authored
-
Johannes Hostert authored
-
Johannes Hostert authored
-
Johannes Hostert authored
-
Johannes Hostert authored
-
Johannes Hostert authored
-
- Nov 06, 2023
-
-
Ralf Jung authored
-
Ralf Jung authored
rename head_step → base_step See merge request iris/iris!1012
-
Ralf Jung authored
-
Ralf Jung authored
rename mapsto → pointsto Closes #495 See merge request iris/iris!1013
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Tweak lemmas for discrete and total `cmra_update` See merge request iris/iris!1016
-
Robbert Krebbers authored
-
Robbert Krebbers authored
`cmra_discrete_updateP` → `cmra_discrete_total_updateP`; repurpose existing lemmas for version with only `CmraDiscrete`.
-
Ralf Jung authored
-
Ralf Jung authored
Fixed iFrame under ∧ and ∨ taking forever to fail in the presence of evars See merge request iris/iris!989
-
Ike Mulder authored
-
Ike Mulder authored
-
- Nov 01, 2023
-
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Robbert Krebbers authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
- Oct 30, 2023
-
-
Ralf Jung authored
Adapt to https://github.com/coq/coq/pull/14928 See merge request iris/iris!1015
-
- Oct 24, 2023
-
-
Ralf Jung authored
Followup 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
-
