diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index b3076cfc543c54b48c0d755bb77b10c965b70953..06e5ef4c6d26c07043bb5dd26359d5f12ce16217 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 Σ).