From a9c5bc545eeda54cda12d459a28d9ba54d794141 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Jan 2017 18:19:28 +0100
Subject: [PATCH] simplify an inG proof

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

diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 18c37ea8b..663ec9412 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -18,7 +18,7 @@ Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
 Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. intros ?%subG_inG. split; apply _. Qed.
 
 Section proof.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).
-- 
GitLab