From f4dc9fc01e0d35538a48fde83af1a818d5e41471 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 24 May 2018 10:45:16 +0200
Subject: [PATCH] Update coqproject.
---
_CoqProject | 1 +
theories/lang/lock.v | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/_CoqProject b/_CoqProject
index a8156fdf..1cd9e93a 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 cf2c520e..1c578eec 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.
--
GitLab