Skip to content
Snippets Groups Projects
Commit 5aa2026c authored by Hai Dang's avatar Hai Dang
Browse files

Bump Iris

parent 52f6028a
No related branches found
No related tags found
No related merge requests found
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
"coq-iris" { (= "dev.2019-05-28.2.e4644041") | (= "dev") }
]
......@@ -215,7 +215,7 @@ Section heap.
{[l + i := (q, Cinr 0%nat, to_agree v)]}).
Proof.
rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
by rewrite /auth_frag (big_opL_commute (Auth None)) big_opL_commute1 //.
rewrite (big_opL_commute auth_frag) big_opL_commute1 //.
Qed.
Global Instance heap_mapsto_pred_fractional l (P : list val iProp Σ):
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment