Skip to content
Snippets Groups Projects
Commit 1b8cc687 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies; fix for auth change

parent a35e41df
No related branches found
No related tags found
No related merge requests found
......@@ -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-09-15.3.986a8883") | (= "dev") }
"coq-iris" { (= "dev.2020-09-30.0.fe735a96") | (= "dev") }
]
......@@ -64,7 +64,7 @@ Section contribution.
Proof.
rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
iDestruct (own_valid_2 with "Hs Hc")
as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid; first done.
as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
by destruct (Pos.lt_irrefl 1).
Qed.
......@@ -89,7 +89,7 @@ Section contribution.
- iDestruct "Hs" as "(_ & _ & Hc')".
by iDestruct (own_valid_2 with "Hc Hc'") as %?.
- iDestruct (own_valid_2 with "Hs Hc")
as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid.
as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
by destruct n.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment