diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3536cf4019750c76a0c760f399dea218c5f9e328..a199aaa80725e864467634504b44275cb69f5c1b 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 d55fea490c396e7711ee8cbc113d6f246f1fbcfd..7d4cd6154294132d3b71d7f16c7bd8f8d2382eef 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 8aee1924bb7256c1691f78a3bdf35e523f97017c..a7ba3898b9a1b2bab152e941895d1a59f12109ad 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 #()