- Aug 04, 2023
-
-
Robbert Krebbers authored
-
- Aug 03, 2023
-
-
Robbert Krebbers authored
Some documentation about `Params` and `Proper`. See merge request iris/iris!962
-
Robbert Krebbers authored
-
Ralf Jung authored -
Robbert Krebbers authored
-
Ralf Jung authored
add more option-included lemmas See merge request iris/iris!957
-
Ralf Jung authored
Use Ltac2 to avoid unrolling tactic notations with lists. See merge request iris/iris!931
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Rodolphe Lepigre authored
-
Jan-Oliver Kaiser authored
-
Robbert Krebbers authored
Revise the theory of the monotone CMRA See merge request iris/iris!950
-
Ralf Jung authored
add agree_valid_included See merge request iris/iris!958
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
add pair_dist See merge request iris/iris!961
-
Ralf Jung authored
-
- Jul 27, 2023
- Jul 25, 2023
-
-
Ralf Jung authored
rename `singleton_mono` to `singleton_included_mono` See merge request iris/iris!955
-
Ralf Jung authored
Add fupd_plain_soundness_no_lc_strong See merge request iris/iris!857
-
-
