diff --git a/algebra/cmra.v b/algebra/cmra.v
index a89f705322f74e605aa9cc118d31b0c6547a487b..b3f8f94b7f29360375776c6872ea8acdc77619e0 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -138,6 +138,8 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 }.
 
 (** * Local updates *)
+(** The idea is that lemams taking this class will usually have L explicit,
+    and leave Lv implicit - it will be inferred by the typeclass machinery. *)
 Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
   local_update_ne n :> Proper (dist n ==> dist n) L;
   local_updateN n x y : Lv x → ✓{n} (x ⋅ y) → L (x ⋅ y) ≡{n}≡ L x ⋅ y