From 395e09189c53c1f675a1fb86f29d335d61dcff4a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2016 15:12:03 +0100
Subject: [PATCH] prove pvs_alloc

---
 program_logic/namespace.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 5f26e17f1..95a475b6b 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -113,7 +113,7 @@ Qed.
 Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
 Proof.
   rewrite /inv (pvs_allocI N); first done.
-  (* FIXME use coPset_suffixes_infinite. *)
-Abort.
+  apply coPset_suffixes_infinite.
+Qed.
 
 End inv.
-- 
GitLab