diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 6cbe7c8a15ce6adaac04b2fff26e80b876f002e1..caf20f26cc8d0e217033c52f15f1a026cf31dbec 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -37,7 +37,7 @@ Section lockG_rules.
 
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
+  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
   Proof. solve_proper. Qed.
 
   Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).