From adc0a0954462f9483be8685f3792187f60a07adf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Dec 2017 11:31:53 +0100
Subject: [PATCH] Make `lock` instances canonical structures.

---
 theories/heap_lang/lib/spin_lock.v   | 4 ++--
 theories/heap_lang/lib/ticket_lock.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 9da9bb33f..23b63251c 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -36,7 +36,7 @@ Section proof.
 
   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.
 
   (** The main proofs. *)
@@ -90,6 +90,6 @@ End proof.
 
 Typeclasses Opaque is_lock locked.
 
-Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7a9f78cd8..7437f7483 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -166,6 +166,6 @@ End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
-- 
GitLab