From d436e40c3fd91040e14e98dad99db0b0da3eabd6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 10:40:52 +0100
Subject: [PATCH] avoid by in tactics (as advised by Robbert)

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

diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1ec6d231a..e98400488 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -4,12 +4,12 @@ Import uPred.
 Ltac wp_strip_later :=
   match goal with
   | |- ∀ _, _ => let H := fresh in intro H; wp_strip_later; revert H
-  | |- _ ⊑ ▷ _ => etransitivity; [|by apply later_intro]
+  | |- _ ⊑ ▷ _ => etransitivity; [|solve [ apply later_intro] ]
   end.
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etransitivity; [|by apply (wp_bind K)]; simpl
+  | _ => etransitivity; [|solve [ apply (wp_bind K) ]]; simpl
   end.
 Ltac wp_finish :=
   let rec go :=
-- 
GitLab