Commit 2affa042 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 473ba705
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") }
"coq-iris" { (= "dev.2021-02-16.0.8ee71fff") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -285,7 +285,7 @@ Proof.
(* close the invariant (in fact, this is not required): *)
iMod ("InvClose" with "[-]") as "_" ; first by auto with iFrame.
(* conclude: *)
iMod (fupd_intro_mask' ) as "_" ; first done. iPureIntro.
iMod (fupd_mask_subseteq ) as "_" ; first done. iPureIntro.
lia.
Qed.
......
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