diff --git a/_CoqProject b/_CoqProject index a8156fdf6a0096eb5bdaad53dd2800d5e9c5e314..1cd9e93ada52e25e0b3421c75f9b8bc62056a450 100644 --- a/_CoqProject +++ b/_CoqProject @@ -19,6 +19,7 @@ theories/lang/notation.v theories/lang/memcpy.v theories/lang/new_delete.v theories/lang/swap.v +theories/lang/lock.v theories/typing/base.v theories/typing/lft_contexts.v theories/typing/type.v diff --git a/theories/lang/lock.v b/theories/lang/lock.v index cf2c520e02265bbf097bbbd3ee62c03b470e8ff2..1c578eecdf5eea3280c8740f2a7917c454a22fa2 100644 --- a/theories/lang/lock.v +++ b/theories/lang/lock.v @@ -74,7 +74,7 @@ Section proof. Proof. by iIntros "#$". Qed. (** The main proofs. *) - Lemma lock_proto_create (R : vProp) l (b : bool) : + Lemma lock_proto_create (R : vProp) l (b : bool) : l ↦ #b -∗ (if b then True else ▷ R) ==∗ ∃ γ, lock_proto_lc l γ R R ∗ ▷ lock_proto_inv l γ R. Proof.