diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 3f65239d370aa0d8241d9e0dc3ac7f9d6de51de1..814bf3224fc636e4f5480dd552be77e92e3736ee 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -93,7 +93,7 @@ Section frac_auth.
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
-  Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
+  Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a  : A) :
     CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.