From afa8efc2b19c1c7dedc657f7a6ae7fc46b0ea5cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Feb 2016 12:40:08 +0100
Subject: [PATCH] Use ewp tactic in heap_lang/tests.
---
heap_lang/tests.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 48753a97c..91021e180 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -65,9 +65,9 @@ Section LiftingTests.
- wp_op. wp_op.
(* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
are goals being generated. That should not be the case. *)
- wp_focus (FindPred _ _). rewrite -FindPred_spec; last by omega.
+ ewp apply FindPred_spec; last omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- - rewrite -FindPred_spec; eauto with omega.
+ - by ewp apply FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
--
GitLab