From 7827f6887a78f41a248ba666bced8a926157d26f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 10:05:54 +0100
Subject: [PATCH] some playing around with wp_tactics
---
heap_lang/tests.v | 2 +-
heap_lang/wp_tactics.v | 5 ++---
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 1502ce450..d3c948d43 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -84,7 +84,7 @@ Section LiftingTests.
True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
Proof.
intros E.
- wp_focus (Pred '42); rewrite -Pred_spec -later_intro.
+ wp_focus (Pred _); rewrite -Pred_spec -later_intro.
wp_rec. rewrite -Pred_spec -later_intro; auto with I.
Qed.
End LiftingTests.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c88954726..164bb9b48 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; [|apply later_intro]
+ | |- _ ⊑ ▷ _ => etransitivity; [|by apply later_intro]
end.
Ltac wp_bind K :=
lazymatch eval hnf in K with
| [] => idtac
- | _ => etransitivity; [|apply (wp_bind K)]; simpl
+ | _ => etransitivity; [|by apply (wp_bind K)]; simpl
end.
Ltac wp_finish :=
let rec go :=
@@ -44,7 +44,6 @@ Tactic Notation "wp_bin_op" ">" :=
wp_bind K; etransitivity; [|eapply wp_bin_op; reflexivity]; wp_finish
end)
end.
-
Tactic Notation "wp_bin_op" := wp_bin_op>; wp_strip_later.
Tactic Notation "wp_un_op" ">" :=
match goal with
--
GitLab