From 95f2133a0c2014681bb723f8f34e8082c0fe8856 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Nov 2020 14:34:16 +0100
Subject: [PATCH] Fix instance arguments so it compiles with recent Coq.

---
 theories/lib/lock.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 6cbe7c8..caf20f2 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).
-- 
GitLab