From fd84063097c4097e4c4a545ca1dde106301787a9 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sun, 6 Sep 2020 02:10:00 +0200
Subject: [PATCH] fix update dep
---
theories/lang/lock.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index b3076cfc..06e5ef4c 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -27,7 +27,7 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
Section proof.
- Context `{noprolG Σ, !lftG view_Lat (↑histN) Σ, lockG Σ}.
+ Context `{noprolG Σ, !lftG (view_Lat loc) (↑histN) Σ, lockG Σ}.
Implicit Types (l : loc).
Local Notation vProp := (vProp Σ).
--
GitLab