From d10c1878595f001d5f60d38e9fa12eea572131cf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 23:40:31 +0100
Subject: [PATCH] Make wp_rec/wp_lam solve to_of_val premises.
---
heap_lang/wp_tactics.v | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 360b44585..d36dd8d50 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -29,7 +29,9 @@ Tactic Notation "wp_rec" ">" :=
| |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
| App (Rec _ _ _) _ =>
- wp_bind K; etrans; [|eapply wp_rec; reflexivity]; wp_finish
+ wp_bind K; etrans;
+ [|eapply wp_rec; repeat (reflexivity || rewrite /= to_of_val)];
+ wp_finish
end)
end).
Tactic Notation "wp_rec" := wp_rec>; try strip_later.
@@ -39,7 +41,9 @@ Tactic Notation "wp_lam" ">" :=
| |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
| App (Rec "" _ _) _ =>
- wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
+ wp_bind K; etrans;
+ [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
+ wp_finish
end)
end.
Tactic Notation "wp_lam" := wp_lam>; try strip_later.
--
GitLab