From 3c30c5c8165ac68665ad7c6e3312c16266a54f9a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 May 2023 13:35:34 +0200
Subject: [PATCH] Normalize statements before `iIntoValid`.
This fixes the second bug in issue #520.
---
iris/proofmode/ltac_tactics.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 86be845c6..63edca3ef 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -827,6 +827,11 @@ time.
*)
Ltac iIntoEmpValid_go :=
lazymatch goal with
+ | |- IntoEmpValid (let _ := _ in _) _ =>
+ (* Normalize [let] so we don't need to rely on type class search to do so.
+ Letting type class search do so is unreliable, see Iris issue #520, and test
+ [test_apply_wand_below_let]. *)
+ lazy zeta; iIntoEmpValid_go
| |- IntoEmpValid (?φ → ?ψ) _ =>
(* Case [φ → ψ] *)
(* note: the ltac pattern [_ → _] would not work as it would also match
--
GitLab