From fda809652054c7c80fe049eab6cabd62b1300633 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Sep 2017 00:14:10 +0200
Subject: [PATCH] Fix regression caused by e17ac4ad and another similar bug.

---
 theories/proofmode/tactics.v | 21 +++++++++++----------
 theories/tests/proofmode.v   | 12 ++++++++++++
 2 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2983b97c1..c9379be10 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -535,16 +535,17 @@ a goal [P] for non-dependent arguments [x_i : P]. *)
 Tactic Notation "iIntoValid" open_constr(t) :=
   let rec go t :=
     let tT := type of t in
-    first
-      [apply (proj1 (_ : AsValid tT _) t)
-      |lazymatch eval hnf in tT with
-       | ?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. *)
-         (* This is a workarround for Coq bug #4969. *)
-         let e := fresh in evar (e:id T);
-         let e' := eval unfold e in e in clear e; go (t e')
-       end] in
+    lazymatch eval hnf in tT with
+    | ?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. *)
+      (* This is a workarround for Coq bug #4969. *)
+      let e := fresh in evar (e:id T);
+      let e' := eval unfold e in e in clear e; go (t e')
+    | _ =>
+      let tT' := eval cbv zeta in tT in apply (proj1 (_ : AsValid tT' _) t)
+      || fail "iPoseProof: not a uPred"
+    end in
   go t.
 
 (* The tactic [tac] is called with a temporary fresh name [H]. The argument
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c9afe2d6e..e09f3f234 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -201,6 +201,18 @@ Lemma test_True_intros : (True : uPred M) -∗ True.
 Proof.
   iIntros "?". done.
 Qed.
+
+Lemma test_iPoseProof_let 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 := True%I in P -∗ R -∗ Q -∗ P ∗ Q.
+Proof. iIntros (Q R) "$ HR $". Qed.
 End tests.
 
 Section more_tests.
-- 
GitLab