diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v index 422f8d8b51330b4e505f6c281fef1078aa42a8fc..67f1338512d502747c217e785bcb0a3db0cd69ed 100644 --- a/theories/heap_lang/lib/lock.v +++ b/theories/heap_lang/lib/lock.v @@ -1,4 +1,4 @@ -From iris.heap_lang Require Export op_rules notation. +From iris.heap_lang Require Export lifting notation. From iris.base_logic.lib Require Export invariants. Structure lock Σ `{!heapG Σ} := Lock {