Commit 87e73ac6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 0b503c78
Pipeline #58996 passed with stage
in 20 minutes and 24 seconds
......@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
synopsis: "Local Simulation proofs, the Iris style"
depends: [
"coq-iris" { (= "dev.2021-11-25.0.b01aa338") | (= "dev") }
"coq-iris" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.2.4+8.12") | (= "1.3+8.14") }
]
......
......@@ -226,7 +226,7 @@ Lemma list_find_proper {A : Type} (P Q : A → Prop)
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x y IH]; [done|]. simpl.
erewrite (decide_iff (P x) (Q x)) by done. by rewrite IH.
erewrite (decide_ext (P x) (Q x)) by done. by rewrite IH.
Qed.
Lemma list_fmap_omap {A B C : Type} (f : A option B) (g : B C) (l : list A) :
......
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