From efa43aa3faf242c60a5fc77fd6e6056d21614888 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Jun 2016 11:37:46 +0200
Subject: [PATCH] Fix type in lock.

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

diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 4404e0fb1..eb11bbb58 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -12,7 +12,7 @@ Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
-Class lockG Σ := SpawnG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
+Class lockG Σ := LockG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
 Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
 Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ.
 Proof. destruct H. split. apply: inGF_inG. Qed.
-- 
GitLab