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

Bump Iris.

parent b040f68f
Pipeline #19816 failed with stage
in 8 minutes and 49 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-06-26.0.ad3e5066") | (= "dev") }
"coq-iris" { (= "dev.2019-08-13.5.c1d6ef7f") | (= "dev") }
]
......@@ -141,7 +141,7 @@ Proof.
set (f i := cmra_extend n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
set (f_proj i := proj1_sig (f i)).
exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
repeat split; intros i; rewrite /= ?lookup_op !map_lookup_imap.
+ destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
rewrite -Hx; apply (proj2_sig (f i)).
+ destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
......
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