Commit eee1edcb authored by Ralf Jung's avatar Ralf Jung

update dependencies

parent 80987bc9
Pipeline #36093 failed with stage
in 14 minutes and 56 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" { (= "dev.2020-10-10.0.cb8e35b8") | (= "dev") }
"coq-iris" { (= "dev.2020-10-13.1.5558d66d") | (= "dev") }
]
......@@ -369,7 +369,7 @@ Section properties.
lv', lv lv' σ !! cl = Some (lv', v).
Proof.
rewrite singleton_included_l=> -[[[q' lv'] av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
rewrite lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
Qed.
......
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