From 777697561f8719d677d0c7a84d89f8d7e91902ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 20:05:57 +0100
Subject: [PATCH] avoid rewrite in tactics, for additional robustness

---
 heap_lang/wp_tactics.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 6cb031f74..1ecf5771d 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -56,7 +56,8 @@ Ltac uLöb tac :=
                let H := fresh in intro H; go; revert H
       | |- ▷ ?R ⊑ (?L -★ locked _) => apply wand_intro_l;
                (* TODO: Do sth. more robust than rewriting. *)
-               trans (▷ (L ★ R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
+               trans (▷ L ★ ▷ R)%I; first (apply sep_mono_l, later_intro; reflexivity);
+               trans (▷ (L ★ R))%I; first (apply equiv_spec, later_sep; reflexivity );
                unlock; tac
       end
   in go.
-- 
GitLab