diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 85e2b334696d2fa2a0af9d1c6bee29394ef9840f..93e3c72ebb584884afb9317cd2f0947db0041215 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -25,7 +25,6 @@ Instance: Params (@uPred_big_sep) 1.
 Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
 
 (** * Other big ops *)
-(** We use a type class to obtain overloaded notations *)
 Definition uPred_big_sepM {M} `{Countable K} {A}
     (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
   [★] (curry Φ <$> map_to_list m).