From 79b13da506c2fa25b3d95a3ef1ee6683a97408c0 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 21 Aug 2019 18:02:13 -0400
Subject: [PATCH] Bumped some re-ordered rewrites and dep versions
---
README.md | 4 ++--
theories/utils/contribution.v | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index c6284fb..8faad22 100644
--- a/README.md
+++ b/README.md
@@ -7,9 +7,9 @@ It has been built and tested with the following dependencies
- Coq 8.9.1
- [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) at
- commit 5f2a6b77.
+ commit f9830af6.
- [iris](https://gitlab.mpi-sws.org/iris/iris) at
- commit 4a624063.
+ commit 0c4e2984.
In order to build, install the above dependencies and then run
`make -j [num CPU cores]` to compile Actris.
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index daffe13..c221ed5 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -94,7 +94,7 @@ Section contribution.
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 -(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. }
by apply option_local_update, csum_local_update_l, prod_local_update_2.
Qed.
@@ -113,7 +113,7 @@ Section contribution.
iApply (own_update_2 with "Hs Hc"). apply auth_update_dealloc.
rewrite -(right_id _ _ (Some (Cinl (1%positive, _)))).
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.
Lemma update_client γ n x y x' y' :
--
GitLab