diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 0db38d070637d9c4a92531a309208afc1931eb7e..3f1c99a1055baa5c832166f5d1d34ba4e064bbdd 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -960,9 +960,9 @@ Section positive.
     - intros ???. apply Pos.add_assoc.
     - intros ??. apply Pos.add_comm.
   Qed.
-  Canonical Structure posR : cmraT := discreteR positive pos_ra_mixin.
+  Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
 
-  Global Instance pos_cmra_discrete : CMRADiscrete posR.
+  Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
   Proof. constructor; apply _ || done. Qed.
 End positive.