Merge requests · Iris / lambda-rust

Add lemmas used by RefinedRust

!38 · created Jul 19, 2024 by Lennard Gäher
- Merged
- 9
updated Aug 31, 2024
Fix proof after iris/iris!1035.

!36 · created Mar 06, 2024 by Ike Mulder
- Merged
- 1
updated Mar 06, 2024
Fix broken proofs for improved iFrame ∃

!35 · created Feb 16, 2024 by Ike Mulder
- Merged
updated Feb 16, 2024
bump to Coq 8.18

!33 · created Oct 02, 2023 by Ralf Jung masters/weak_mem
- Merged
updated Oct 02, 2023
update to Coq 8.18

!32 · created Sep 29, 2023 by Ralf Jung
- Merged
updated Sep 29, 2023
Made refcell state coercion implementation agnostic

!31 · created Aug 21, 2023 by Ike Mulder
- Merged
updated Aug 21, 2023
Enable mangled names

!30 · created May 29, 2023 by Hai Dang masters/weak_mem
- Merged
updated May 29, 2023
fixes for iris/iris!886 and iris/iris!896

!29 · created Mar 07, 2023 by Simon Spies masters/weak_mem
- Merged
updated Mar 08, 2023
fix for iris!886 and iris!896

!28 · created Feb 02, 2023 by Michael Sammler
- Merged
- 6
updated Mar 08, 2023
Parameterize the lifetime logic over the user mask.

!24 · created May 04, 2021 by Jacques-Henri Jourdan
- Merged
- 22
updated May 19, 2021
Improve notations for functions

!23 · created May 01, 2021 by Jacques-Henri Jourdan
- Merged
- 4
- 1
updated May 07, 2021
add GhostCell proof 4 of 4 checklist items completed

!19 · created Mar 09, 2021 by Ralf Jung
- Merged
- 21
updated Mar 16, 2021
Update iris dependency

!22 · created Mar 16, 2021 by Michael Sammler
- Merged
- 1
updated Mar 16, 2021
prove model for own_ptr

!18 · created Mar 01, 2021 by Xavier Denis rusthornbelt
- Merged
- 3
updated Mar 02, 2021
Fix typos

!17 · created Oct 29, 2020 by Yusuke Matsushita
- Merged
- 1
updated Oct 29, 2020
fill in blanks in LICENSE

!15 · created Mar 13, 2020 by Ralf Jung
- Merged
- 2
updated Mar 14, 2020
fill in blanks in LICENSE

!16 · created Mar 13, 2020 by Ralf Jung masters/weak_mem
- Merged
- 1
updated Mar 14, 2020
Adapt to coq/coq#8829 (Error when [foo.(bar)] is used with nonprojection [bar])

!13 · created Feb 18, 2019 by Gaëtan Gilbert
- Merged
- 6
updated Feb 20, 2019
Bump Iris version

!12 · created Feb 04, 2019 by Maxime Dénès
- Merged
- 1
updated Feb 04, 2019
Make trivial instances explicit

!11 · created Jan 24, 2019 by Maxime Dénès
- Merged
- 1
updated Jan 24, 2019