From e6d754c7bf712603205cf2b4b42e60d069da34e4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 09:46:39 +0100
Subject: [PATCH] get rid of an aborted lemma

---
 program_logic/ghost_ownership.v | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 64594e729..2d35bebb8 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -52,11 +52,6 @@ Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ✓ a).
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
-Lemma own_empty `{CMRAUnit A} γ : True ⊢ own γ ∅.
-Proof.
-  rewrite ownG_empty /own. apply equiv_spec, ownG_proper.
-  (* FIXME: rewrite to_globalF_empty. *)
-Abort.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. unfold own; apply _. Qed.
 Global Instance own_core_always_stable γ a : AlwaysStable (own γ (core a)).
-- 
GitLab