From fa0b270b3c9c7f9d3962adeb104a8a09deaa050d Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 21 Sep 2020 18:11:26 -0500
Subject: [PATCH] Report an error when iIntro fails to find a forall

The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.
---
 tests/proofmode.ref               | 4 ++++
 tests/proofmode.v                 | 7 +++++++
 theories/proofmode/ltac_tactics.v | 2 +-
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 8ddfcb423..393eada00 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -541,6 +541,10 @@ The command has indeed failed with message:
 Tactic failure: iIntro: "HP" not fresh.
 The command has indeed failed with message:
 x is already used.
+"iIntros_pure_not_forall"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: cannot turn (P -∗ Q)%I into a universal quantifier.
 "iSplitL_one_of_many"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d84511d9d..cee968cb6 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1104,6 +1104,13 @@ Proof.
   iIntros "HQ" (x). Fail iIntros (x).
 Abort.
 
+Check "iIntros_pure_not_forall".
+Lemma iIntros_pure_not_forall P Q :
+  P -∗ Q.
+Proof.
+  Fail iIntros (?).
+Abort.
+
 Check "iSplitL_one_of_many".
 Lemma iSplitL_one_of_many P :
   P -∗ P -∗ P ∗ P.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2a4018986..1aebf309c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -472,7 +472,7 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
     | |- envs_entails _ _ =>
       eapply tac_forall_intro;
         [iSolveTC ||
-         let P := match goal with |- FromForall ?P _ => P end in
+         let P := match goal with |- FromForall ?P _ _ => P end in
          fail "iIntro: cannot turn" P "into a universal quantifier"
         |let name := lazymatch goal with
                      | |- let _ := (λ name, _) in _ => name
-- 
GitLab