Test cases.

tests/proofmode.ref

@@ -954,6 +954,16 @@ The command has indeed failed with message:
 Tactic failure: sel_pat.parse: the term m
 is expected to be a selection pattern (usually a string),
 but has unexpected type nat.
+"test_iIntros_let_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: iStartProof: goal is a `let`, use `simpl`,
+`intros x`, `iIntros (x)`, or `iIntros "%x".
+"test_iIntros_let_wand_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: iStartProof: goal is a `let`, use `simpl`,
+`intros x`, `iIntros (x)`, or `iIntros "%x".
 "test_pure_name"
      : string
 1 goal

tests/proofmode.v

@@ -885,11 +885,46 @@ Proof.
   iIntros (help) "HP".
   iPoseProof (help with "[$HP]") as "?". done.
 Qed.
+Lemma test_iPoseProof_let_wand P Q :
+  (let R := True%I in R ∗ P ⊢ Q) →
+  P -∗ Q.
+Proof.
+  iIntros (help) "HP".
+  iPoseProof (help with "[$HP]") as "?". done.
+Qed.
+
+Lemma test_iPoseProof_let_in_string P Q :
+  (let R := True%I in R ∗ P ⊢ Q) →
+  P ⊢ Q.
+Proof.
+  iIntros "%help HP".
+  iPoseProof (help with "[$HP]") as "?". done.
+Qed.
 
 Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
+Lemma test_iIntros_let_wand P :
+  ∀ Q, let R := emp%I in P ⊢ R -∗ Q -∗ P ∗ Q.
+Proof. iIntros (Q R) "$ _ $". Qed.
+
+Lemma lemma_for_test_apply_below_let (Φ : nat → PROP) :
+  let Q := Φ 5 in
+  Q ⊢ Q.
+Proof. iIntros (?) "?". done. Qed.
+Lemma test_apply_below_let (Φ : nat → PROP) :
+  Φ 5 -∗ Φ 5.
+Proof. iIntros "?". iApply lemma_for_test_apply_below_let. done. Qed.
+
+Lemma lemma_for_test_apply_wand_below_let (Φ : nat → PROP) :
+  let Q := Φ 5 in
+  Q -∗ Q.
+Proof. iIntros (?) "?". done. Qed.
+Lemma test_apply_wand_below_let (Φ : nat → PROP) :
+  Φ 5 -∗ Φ 5.
+Proof. iIntros "?". iApply lemma_for_test_apply_wand_below_let. done. Qed.
+
 Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
@@ -1756,6 +1791,22 @@ Proof.
   Fail iInduction n as [|n] "IH" forall m.
 Abort.
 
+Check "test_iIntros_let_fail".
+Lemma test_iIntros_let_fail P :
+  let Q := (P ∗ P)%I in
+  Q ⊢ Q.
+Proof.
+  Fail iIntros "Q".
+Abort.
+
+Check "test_iIntros_let_wand_fail".
+Lemma test_iIntros_let_wand_fail P :
+  let Q := (P ∗ P)%I in
+  Q ⊢ Q.
+Proof.
+  Fail iIntros "Q".
+Abort.
+
 End error_tests.
 
 Section pure_name_tests.