From 463474fb0f5feeb8387fcae225854c4ec7312cf2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 May 2018 12:13:24 +0200
Subject: [PATCH] Rename `frag_auth_op` into `frac_auth_frag_op` (the old name
 was inconsistent).

`sed -i 's/frag_auth_op/frac_auth_frag_op/g' $(find -name "*.v")`
---
 CHANGELOG.md                     | 2 ++
 theories/algebra/frac_auth.v     | 8 ++++----
 theories/heap_lang/lib/counter.v | 2 +-
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3536cf401..a199aaa80 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -22,6 +22,8 @@ Changes in Coq:
   - `IntoLaterN'` → `IntoLaterN` (this one _should_ strip a later)
   - `IntoLaterNEnv` → `MaybeIntoLaterNEnv`
   - `IntoLaterNEnvs` → `MaybeIntoLaterNEnvs`
+* Rename:
+  - `frag_auth_op` → `frac_auth_frag_op`
 * `namespaces` has been moved to std++.
 
 ## Iris 3.1.0 (released 2017-12-19)
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index d55fea490..7d4cd6154 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -81,13 +81,13 @@ Section frac_auth.
   Lemma frac_auth_frag_valid q a : ✓ (◯!{q} a) ↔ ✓ q ∧ ✓ a.
   Proof. done. Qed.
 
-  Lemma frag_auth_op q1 q2 a1 a2 : ◯!{q1+q2} (a1 ⋅ a2) ≡ ◯!{q1} a1 ⋅ ◯!{q2} a2.
+  Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯!{q1+q2} (a1 ⋅ a2) ≡ ◯!{q1} a1 ⋅ ◯!{q2} a2.
   Proof. done. Qed.
 
   Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯!{1} a ⋅ ◯!{q} b) → False.
-  Proof. rewrite -frag_auth_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
+  Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
   Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯!{1} a ⋅ ◯!{q} b) → False.
-  Proof. rewrite -frag_auth_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
+  Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
 
   Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
@@ -97,7 +97,7 @@ Section frac_auth.
     CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
-    by rewrite -frag_auth_op -core_id_dup.
+    by rewrite -frac_auth_frag_op -core_id_dup.
   Qed.
 
   Lemma frac_auth_update q a b a' b' :
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8aee1924b..a7ba3898b 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -105,7 +105,7 @@ Section contrib_spec.
   (** The main proofs. *)
   Lemma ccounter_op γ q1 q2 n1 n2 :
     ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2.
-  Proof. by rewrite /ccounter frag_auth_op -own_op. Qed.
+  Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed.
 
   Lemma newcounter_contrib_spec (R : iProp Σ) :
     {{{ True }}} newcounter #()
-- 
GitLab