Skip to content
Snippets Groups Projects
Commit 90bc7991 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent dca7dfd7
Branches
Tags
No related merge requests found
...@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries. ...@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
""" """
depends: [ depends: [
"coq-iris" { (= "dev.2022-06-28.0.b337ca8c") | (= "dev") } "coq-iris" { (= "dev.2022-07-05.1.a32f36a9") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
...@@ -21,7 +21,7 @@ Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ : ...@@ -21,7 +21,7 @@ Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
( `{!lrustGS Σ}, True WP e {{ v, φ v }}) ( `{!lrustGS Σ}, True WP e {{ v, φ v }})
adequate NotStuck e σ (λ v _, φ v). adequate NotStuck e σ (λ v _, φ v).
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??). intros Hwp; eapply (wp_adequacy_lc _ _); iIntros (???).
iMod (own_alloc ( to_heap σ)) as () "Hvγ". iMod (own_alloc ( to_heap σ)) as () "Hvγ".
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. } { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc ( ( : heap_freeableUR))) as () "Hfγ"; iMod (own_alloc ( ( : heap_freeableUR))) as () "Hfγ";
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment