Commit 1ca3eaa6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 85307154
Pipeline #15565 failed with stage
in 17 minutes and 3 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-02-22.1.9c04e2b4") | (= "dev") }
"coq-iris" { (= "dev.2019-03-05.0.38abc449") | (= "dev") }
]
......@@ -288,7 +288,7 @@ Proof.
Qed.
Section freshness.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Context `{Infinite K}.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : gset K) m x :
x ( i, m !! i = None i I Q (<[i:=x]>m)) m ~~>: Q.
Proof.
......
......@@ -62,7 +62,7 @@ Section gset.
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Context `{Infinite K}.
Arguments op _ _ _ _ : simpl never.
Lemma gset_alloc_updateP_strong (Q : gset_disj K Prop) (I : gset K) X :
......
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