Commit 47b09af3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 9411225c
Pipeline #14820 passed with stage
in 14 minutes and 20 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-01-15.0.85509592") | (= "dev") }
"coq-iris" { (= "dev.2019-02-06.0.4f086f68") | (= "dev") }
]
......@@ -97,8 +97,8 @@ Proof.
- rewrite ownG_empty. eapply pvs_ownG_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, γ, γ G iprod_singleton (inG_id i) y = to_globalF γ a)).
* rewrite -ucmra_transport_unit.
eapply ucmra_transport_updateP. eapply alloc_updateP_strong'; eauto.
* rewrite -(ucmra_transport_unit inG_prf).
eapply ucmra_transport_updateP; first by eapply alloc_updateP_strong'; eauto.
intros ? (γ&?&?&?); subst.
exists γ. split_and!; eauto.
* naive_solver.
......
Markdown is supported
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