From 061686bf89ee4eebaa6cf318cef0f7ef74fe0a4e Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 23 Apr 2020 13:01:34 +0200
Subject: [PATCH] Rename auth_both_frac_op to auth_both_op

Removes auth_both_op and renames auth_both_frac_op into auth_both_op.
---
 CHANGELOG.md            | 3 +++
 theories/algebra/auth.v | 6 ++----
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c852bbbd..5cf35a15f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -150,6 +150,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
     - `|={E1,E2}|>=>^n Q` for `|={E1,E2}â–·=>^n Q`
     The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v),
     where the ASCII notations are defined in terms of the unicode notations.
+* Removed `auth_both_op` and renamed `auth_both_frac_op` into `auth_both_op`.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -167,6 +168,8 @@ s/\blist_lookup_singletonM(|_lt|_gt|_ne)\b/list_lookup_singleton\1/g
 s/\blist_singletonM_(validN|length)\b/list_singleton_\1/g
 s/\blist_alter_singletonM\b/list_alter_singleton/g
 s/\blist_singletonM_included\b/list_singleton_included/g
+# auth_both_frac_op rename
+s/\bauth_both_frac_op\b/auth_both_op/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c67de2986..0f7132fb1 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -306,10 +306,8 @@ Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
   (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
 Proof. apply (big_opMS_commute _). Qed.
 
-Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b.
+Lemma auth_both_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
-Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b.
-Proof. by rewrite auth_both_frac_op. Qed.
 
 Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
 Proof.
@@ -348,7 +346,7 @@ Proof. by rewrite auth_validI. Qed.
 Lemma auth_both_validI {M} q (a b: A) :
   ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
 Proof.
-  rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|].
+  rewrite -auth_both_op auth_validI /=. apply bi.and_proper; [done|].
   setoid_rewrite agree_equivI. iSplit.
   - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H".
     iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto.
-- 
GitLab