From 3a18b722c9cfd725b43e547407aa7bb22f2c4e04 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Feb 2016 12:03:08 +0100
Subject: [PATCH] Remove FIXME.

---
 program_logic/viewshifts.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index db9e9ccd3..927fcb27a 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -92,9 +92,7 @@ Lemma vs_open_close N E P Q R :
 Proof.
   intros; apply (always_intro _ _), impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  (* FIXME sep_elim_l' is already added to the DB in upred.v. Why do
-     I have to mention it here again? *)
-  apply: (pvs_open_close E N); [by eauto using sep_elim_l'..|].
+  eapply pvs_open_close; [by eauto using sep_elim_l'..|].
   rewrite sep_elim_r. apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
   rewrite assoc -always_and_sep_r'.
-- 
GitLab