From 7cf966c4b3f2f7ca88e087fecfb1889810da8c4b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Aug 2016 15:49:42 +0200
Subject: [PATCH] Make iIntoEntails work when the entails is hidden under a
delta.
---
proofmode/tactics.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ce4c4ca88..8d4dfdade 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -221,10 +221,12 @@ The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoEntails" open_constr(t) :=
let rec go t :=
- lazymatch type of t with
+ let tT := type of t in
+ lazymatch eval hnf in tT with
| True ⊢ _ => apply t
| _ ⊢ _ => apply (uPred.entails_wand _ _ t)
- | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
+ (* need to use the unfolded version of [⊣⊢] due to the hnf *)
+ | uPred_equiv' _ _ => apply (uPred.equiv_iff _ _ t)
| ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
| ∀ _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
--
GitLab