Commit b040f68f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 35608312
Pipeline #19022 failed with stage
in 9 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-18.6.7a983818") | (= "dev") }
"coq-iris" { (= "dev.2019-06-26.0.ad3e5066") | (= "dev") }
]
......@@ -284,8 +284,7 @@ Proof.
- eapply Hclosing=>x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
exists (x, es); split; auto. rewrite elem_of_map_to_list //.
- set_unfold. intros x (_&Hnin).
intros ((?&es)&?&?%elem_of_map_to_list)%elem_of_list_fmap.
- set_unfold. intros x (_&Hnin) ((?&es)&?&?%elem_of_map_to_list).
subst. eapply Hnin. apply elem_of_dom; eauto.
Qed.
......
......@@ -284,8 +284,7 @@ Proof.
- eapply Hclosing=>x. rewrite elem_of_dom.
intros (es&Hlook). apply elem_of_list_fmap.
exists (x, es); split; auto. rewrite elem_of_map_to_list //.
- set_unfold. intros x (_&Hnin).
intros ((?&es)&?&?%elem_of_map_to_list)%elem_of_list_fmap.
- set_unfold. intros x (_&Hnin) ((?&es)&?&?%elem_of_map_to_list).
subst. eapply Hnin. apply elem_of_dom; eauto.
Qed.
......
......@@ -330,10 +330,7 @@ Section bounded_nondet_hom2.
edestruct (Hin (Some b')) as (ob'' & Hequiv & Hb''_in).
{ eexists; eauto. }
inversion Hequiv as [? b''|]; subst.
exists b''; split; eauto.
unfold l'.
eapply (elem_of_map (λ ob, match ob with | None => b | Some b' => b' end) _ (Some b''));
auto.
exists b''; split; eauto. by eexists (Some _).
Qed.
Lemma isteps_wptp_comp_hom2 i tσ1 tσ2 ob1:
......
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