- Mar 09, 2023
-
-
- Mar 07, 2023
-
-
Robbert Krebbers authored
Rename `f_contractive_core` into `dist_later_intro`. See merge request iris/iris!896
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Change definition of dist_later for compatability with Transfinite Iris See merge request iris/iris!886
-
-
- Mar 05, 2023
-
-
Robbert Krebbers authored
-
- Mar 04, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 03, 2023
-
-
Robbert Krebbers authored
Prove that invariants are "except 0". See merge request iris/iris!897
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 01, 2023
-
-
Robbert Krebbers authored
-
- Feb 16, 2023
-
-
Ralf Jung authoredIn logatom lock: Formalize that the lock is Free before acquire. See merge request iris/iris!891
-
Robbert Krebbers authored
-
Ralf Jung authored
Adapt to https://github.com/coq/coq/pull/16788 See merge request iris/iris!893
-
Ralf Jung authored
add big_opM_gset_to_gmap See merge request iris/iris!878
-
Ralf Jung authored
add RA for integers with addition See merge request iris/iris!879
-
-
Ralf Jung authored
-
Ralf Jung authored
-
- Feb 15, 2023
-
-
-
Ralf Jung authored
-
Ralf Jung authored
Stronger version of `gmap_core_id`. See merge request iris/iris!892
-
Robbert Krebbers authored
-
- Feb 14, 2023
-
-
Ralf Jung authored
Extract dfrac notations See merge request iris/iris!756
-
Robbert Krebbers authored
-
- Feb 13, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Adam authored
This fixes the fixme introduced in !554. Coq issue #13654 was fixed by coq pr #14183.
-
- Feb 08, 2023
-
-
Robbert Krebbers authored
Introduce bi_nsteps and add timeless results for bi closures See merge request iris/iris!885
-
-
- Feb 04, 2023
-
-
Ralf Jung authored
-
- Feb 03, 2023
-
-
Ralf Jung authored
drop support for Coq 8.13 See merge request iris/iris!882
-
- Feb 02, 2023
-
-
Ralf Jung authored
Add more primitive projections See merge request iris/iris!873
-
-
- Feb 01, 2023
-
-
Ralf Jung authored
-
Ralf Jung authored
Add comments to explain the modified structure of the adequacy proof See merge request iris/iris!847
-
-
