From 036278e59ff131dcc11013aeef7e78cacdf2d822 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 22:21:18 +0100
Subject: [PATCH] document LocalUpdate usage

---
 algebra/cmra.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index a89f70532..b3f8f94b7 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
-- 
GitLab