From 03b7f9238c30349b25d69ca61702b61c6f0c5739 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 22:14:40 +0100
Subject: [PATCH] reference the coq bug for the idtac weirdness
---
heap_lang/wp_tactics.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index b233e5ab1..93645fda3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -119,12 +119,13 @@ Ltac wp_finish :=
Tactic Notation "wp_rec" ">" :=
u_löb ltac:((* Find the redex and apply wp_rec *)
- idtac; (* FIXME WTF without this, it matches the goal before executing u_löb ?!? *)
+ idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
lazymatch goal with
| |- _ ⊑ 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; reflexivity];
+ wp_finish
end)
end).
Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
--
GitLab