Commit a3346085 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 01d95642
Pipeline #41351 failed with stage
in 14 minutes and 4 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris-heap-lang" { (= "dev.2021-01-26.0.a26cf167") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2021-02-01.1.4c96a504") | (= "dev") }
]
......@@ -493,7 +493,7 @@ Section flock.
- iIntros (i x m' Hi IH) "He".
rewrite fmap_insert insert_union_singleton_l.
assert (({[i := f x]} (f <$> m')) = {[i := f x]} (f <$> m')) as ->.
{ rewrite /op /cmra_op /= /gmap_op.
{ rewrite /op /cmra_op /= /gmap_op_instance.
apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
- etransitivity. eapply lookup_union_Some_l. apply lookup_insert.
symmetry. rewrite lookup_merge lookup_insert.
......
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