From c78daf894453bc14d04b097f54ac88392494e774 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 10:20:14 +0100
Subject: [PATCH] try to rely more on eauto - and fail and leave some FIXMEs

---
 program_logic/viewshifts.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 32a0324c0..0eb96eadb 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -86,13 +86,18 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊑ (P ={E ∪ Ef}=> Q).
 Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 
+(* FIXME: This is needed to make eauto solve [inv N R ⊑ inv N ?c]. *)
+Local Hint Extern 100 (_ ⊑ _) => reflexivity.
+
 Lemma vs_open_close N E P Q R :
   nclose N ⊆ E →
   (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
 Proof.
   intros; apply (always_intro _ _), impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  apply: (pvs_open_close E N); [by eauto using sep_elim_l..|].
+  (* 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'..|].
   rewrite sep_elim_r. apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
   rewrite assoc -always_and_sep_r'.
-- 
GitLab