diff --git a/algebra/cmra.v b/algebra/cmra.v
index f2f0da685f5ccd26beddb65db2bd10a02046619a..2d55bbf362dbcef7abd1886d9e6744ff5adfe279 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -516,7 +516,7 @@ Section discrete.
       apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
-  Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
+  Global Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
   Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
 End discrete.