Commit 79b13da5 authored by Jonas Kastberg's avatar Jonas Kastberg

Bumped some re-ordered rewrites and dep versions

parent 8cb47270
...@@ -7,9 +7,9 @@ It has been built and tested with the following dependencies ...@@ -7,9 +7,9 @@ It has been built and tested with the following dependencies
- Coq 8.9.1 - Coq 8.9.1
- [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at - [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at
commit 5f2a6b77. commit f9830af6.
- [iris](https://gitlab.mpi-sws.org/iris/iris) at - [iris](https://gitlab.mpi-sws.org/iris/iris) at
commit 4a624063. commit 0c4e2984.
In order to build, install the above dependencies and then run In order to build, install the above dependencies and then run
`make -j [num CPU cores]` to compile Actris. `make -j [num CPU cores]` to compile Actris.
......
...@@ -94,7 +94,7 @@ Section contribution. ...@@ -94,7 +94,7 @@ Section contribution.
with (Some (Cinl (Pos.of_nat (S n), x)), Some (Cinl (1%positive, ε))). with (Some (Cinl (Pos.of_nat (S n), x)), Some (Cinl (1%positive, ε))).
{ rewrite Nat2Pos.inj_succ // -Pos.add_1_l -{2}(left_id ε op x). { rewrite Nat2Pos.inj_succ // -Pos.add_1_l -{2}(left_id ε op x).
rewrite -(right_id _ _ (Some (Cinl (1%positive, _)))). rewrite -(right_id _ _ (Some (Cinl (1%positive, _)))).
rewrite -pair_op -Cinl_op Some_op. apply op_local_update_discrete. rewrite pair_op Cinl_op Some_op. apply op_local_update_discrete.
intros [??]; split=> //=. by rewrite left_id. } intros [??]; split=> //=. by rewrite left_id. }
by apply option_local_update, csum_local_update_l, prod_local_update_2. by apply option_local_update, csum_local_update_l, prod_local_update_2.
Qed. Qed.
...@@ -113,7 +113,7 @@ Section contribution. ...@@ -113,7 +113,7 @@ Section contribution.
iApply (own_update_2 with "Hs Hc"). apply auth_update_dealloc. iApply (own_update_2 with "Hs Hc"). apply auth_update_dealloc.
rewrite -(right_id _ _ (Some (Cinl (1%positive, _)))). rewrite -(right_id _ _ (Some (Cinl (1%positive, _)))).
rewrite Nat2Pos.inj_succ // -Pos.add_1_l. rewrite Nat2Pos.inj_succ // -Pos.add_1_l.
rewrite -pair_op -Cinl_op Some_op left_id. apply (cancel_local_update _ _ _). rewrite pair_op Cinl_op Some_op left_id. apply (cancel_local_update _ _ _).
Qed. Qed.
Lemma update_client γ n x y x' y' : Lemma update_client γ n x y x' y' :
......
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