diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index f16c450e468d45fc1a527d940249e6863ad888ca..720dcc19aa4af6c4696ed456ae0167c6f797ac7d 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -34,6 +34,6 @@ Arguments locked {_ _} _ _.
 
 Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N lk R:
-  Proper ((≡) ==> (≡)) (is_lock L N lk R) := ne_proper _.
+Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
+  Proper ((≡) ==> (≡)) (is_lock L N γ lk) := ne_proper _.