Commit 4c96a504 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent b3fa6d5f
......@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
depends: [
"coq" { (>= "8.11" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2021-01-28.1.889d99ae") | (= "dev") }
"coq-stdpp" { (= "dev.2021-02-01.1.bcebd707") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
......
......@@ -409,7 +409,7 @@ Qed.
Lemma dom_op m1 m2 : dom (gset K) (m1 m2) = dom _ m1 dom _ m2.
Proof.
apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
......
......@@ -68,7 +68,7 @@ Proof.
eauto with sts; set_solver.
Qed.
Global Instance frame_step_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /set_equiv_spec [??]; split; by apply frame_step_mono. Qed.
Proof. move=> ?? /set_equiv_subseteq [??]; split; by apply frame_step_mono. Qed.
Local Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
......@@ -81,7 +81,7 @@ Proof.
Qed.
Global Instance up_proper : Proper ((=) ==> () ==> ()) up.
Proof.
by move=> ??? ?? /set_equiv_spec [??]; split; apply up_preserving.
by move=> ??? ?? /set_equiv_subseteq [??]; split; apply up_preserving.
Qed.
Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
Proof.
......@@ -90,7 +90,7 @@ Proof.
Qed.
Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Proof.
move=> S1 S2 /set_equiv_spec [??] T1 T2 /set_equiv_spec [??];
move=> S1 S2 /set_equiv_subseteq [??] T1 T2 /set_equiv_subseteq [??];
split; by apply up_set_preserving.
Qed.
......@@ -155,7 +155,7 @@ Lemma closed_up_empty s : closed (up s ∅) ∅.
Proof. eauto using closed_up with sts. Qed.
Lemma up_closed S T : closed S T up_set S T S.
Proof.
intros ?; apply set_equiv_spec; split; auto using subseteq_up_set.
intros ?; apply set_equiv_subseteq; split; auto using subseteq_up_set.
intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
......
......@@ -1333,7 +1333,7 @@ Section map2.
dom (gset K) m1 = dom (gset K) m2 .
Proof.
rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
apply elem_of_equiv_L=> k. by rewrite !elem_of_dom.
apply set_eq=> k. by rewrite !elem_of_dom.
Qed.
Lemma big_sepM2_flip Φ m1 m2 :
......
Supports Markdown
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