Commit 42e0d03d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 232c2cac
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
"coq-iris" { (= "dev.2020-04-02.5.fa438702") | (= "dev") }
"coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -124,7 +124,7 @@ Section refinement.
rewrite auth_auth_valid. done. }
iPureIntro.
revert Hfoo.
rewrite singleton_included=> -[av []].
rewrite singleton_included_l=> -[av []].
revert Hvalid.
rewrite /to_offer_reg !lookup_fmap.
case: (N !! o)=> [av'|] Hvalid; last by inversion 1.
......
......@@ -113,7 +113,7 @@ Section conversions.
Lemma tpool_singleton_included tp j e :
{[j := Excl e]} to_tpool tp tp !! j = Some e.
Proof.
move=> /singleton_included [ex [/leibniz_equiv_iff]].
move=> /singleton_included_l [ex [/leibniz_equiv_iff]].
rewrite tpool_lookup fmap_Some=> [[e' [-> ->]] /Excl_included ?]. by f_equal.
Qed.
Lemma tpool_singleton_included' tp j e :
......
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