From da22439858554bf5ed6fa3920b04f8ad33fbb132 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 May 2023 13:18:05 +0200
Subject: [PATCH] Make sure that `iStartProof` fails on goals with `let`.
These should either be `simpl`ed or introduced into the Coq context.
Fixes the first bug in issue #520.
---
iris/proofmode/ltac_tactics.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 137683a28..86be845c6 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -66,6 +66,8 @@ Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
(** * Start a proof *)
Tactic Notation "iStartProof" :=
lazymatch goal with
+ | |- (let _ := _ in _) => fail "iStartProof: goal is a `let`, use `simpl`,"
+ "`intros x`, `iIntros (x)`, or `iIntros ""%x"""
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
[tc_solve || fail "iStartProof: not a BI assertion"
--
GitLab