Commits on Source (12)
-
Isaac van Bakel authored
Without this line, mathpartir.sty doesn't get pulled in to the document despite being used for commands in pftools.sty, which is an annoyance.
Verifiedc570be46 -
Paolo G. Giarrusso authoredbd641645
-
Daniel Nezamabadi authored5602833e
-
Robbert Krebbers authored08a7857e
-
Ralf Jung authored
Constrain lock_name to be Inhabited See merge request iris/iris!1089
f9d1e1da -
Ralf Jung authored57fb6a06
-
Robbert Krebbers authored
remove link to iris club mailing list from readme See merge request iris/iris!1091
55b5d676 -
Ralf Jung authored
bupd_alt.v: fix thinko in docs See merge request iris/iris!1088
e3388f1b -
Ralf Jung authored
Add requirement of mathpartir to pftools.sty See merge request iris/iris!1087
6b57ac28 -
Robbert Krebbers authoredf500dc6c
-
Robbert Krebbers authored49759c97
-
Robbert Krebbers authored
Add lemma `ufrac_auth_update_surplus_cancel`. See merge request iris/iris!1092
3c1e0431
Showing
- CHANGELOG.md 10 additions, 0 deletionsCHANGELOG.md
- README.md 3 additions, 4 deletionsREADME.md
- iris/algebra/lib/ufrac_auth.v 24 additions, 4 deletionsiris/algebra/lib/ufrac_auth.v
- iris/base_logic/bupd_alt.v 3 additions, 3 deletionsiris/base_logic/bupd_alt.v
- iris_heap_lang/lib/lock.v 1 addition, 0 deletionsiris_heap_lang/lib/lock.v
- tex/pftools.sty 1 addition, 0 deletionstex/pftools.sty