diff --git a/opam b/opam index 16635d5ffede692e9a1d18b1b4b80d2b69b9f940..9d275d4d4009f3a801744388f6606adb3ca12526 100644 --- a/opam +++ b/opam @@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] install: [make "install"] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ] depends: [ - "coq-iris" { (= "dev.2020-10-10.0.cb8e35b8") | (= "dev") } + "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") } ] diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v index 4615bd9d686e3a60b35e5ea71fbf619ea2d4277b..3b7dec6cf33bfbe26edc4c6f3e02ebe9a89e9e4c 100644 --- a/theories/utils/contribution.v +++ b/theories/utils/contribution.v @@ -87,7 +87,7 @@ Section contribution. Proof. rewrite /server /client. iIntros "Hs Hc". case_decide; subst. - iDestruct "Hs" as "(_ & _ & Hc')". - by iDestruct (own_valid_2 with "Hc Hc'") as %?. + by iDestruct (own_valid_2 with "Hc Hc'") as %?%auth_frag_op_valid_1. - iDestruct (own_valid_2 with "Hs Hc") as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete. { setoid_subst. by destruct n. }