From 87637946e65639f53baf0006107076efcb1f559d Mon Sep 17 00:00:00 2001
From: Joshua Yanovski <pythonesque@gmail.com>
Date: Fri, 14 Jul 2017 14:54:35 +0200
Subject: [PATCH] Fix typo in is_lock_proper for heap_lang.

---
 theories/heap_lang/lib/lock.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index f16c450e4..5796f1f91 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -26,6 +26,8 @@ Structure lock Σ `{!heapG Σ} := Lock {
     {{{ is_lock N γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
 
+
+
 Arguments newlock {_ _} _.
 Arguments acquire {_ _} _.
 Arguments release {_ _} _.
@@ -34,6 +36,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 _.
 
-- 
GitLab