Skip to content
Snippets Groups Projects
Commit f4dc9fc0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Update coqproject.

parent d128a66e
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -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
......
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment