Skip to content
Snippets Groups Projects
Commit 25c37eb0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 7f20c471
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 25c37eb0
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 09d97eae9eba95ebf5539a0b32e88bfc0b61c0fe coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
theories/typing/own.v
+ 1
− 1
View file @ 25c37eb0
...@@ -229,7 +229,7 @@ Section typing. ...@@ -229,7 +229,7 @@ Section typing.
Proof. Proof.
iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton. iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done. wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ". rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; []. iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
rewrite freeable_sz_full. by iFrame. rewrite freeable_sz_full. by iFrame.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment