From 89174aca5ea61e5b7bcaecbc5bf2d87527c52945 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 7 Apr 2020 08:39:38 -0500
Subject: [PATCH] Fix introducing forall with "%" intro pattern

Fixes #307.
---
 tests/proofmode.ref               | 11 +++++++++++
 tests/proofmode.v                 |  9 +++++++++
 theories/proofmode/ltac_tactics.v |  2 +-
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3b5776176..b22f2edf5 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -77,6 +77,17 @@
   --------------------------------------∗
   Q
   
+"test_iIntros_forall_pure"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Ψ : nat → PROP
+  a : nat
+  ============================
+  --------------------------------------∗
+  Ψ a → Ψ a
+  
 The command has indeed failed with message:
 No applicable tactic.
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f4fefc0a5..01e0189a5 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -119,6 +119,15 @@ Proof. iIntros "-#HQ". done. Qed.
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
+Check "test_iIntros_forall_pure".
+Lemma test_iIntros_forall_pure (Ψ: nat → PROP) :
+  ⊢ ∀ x : nat, Ψ x → Ψ x.
+Proof.
+  iIntros "%".
+  (* should be a trivial implication now *)
+  Show. auto.
+Qed.
+
 Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False ⌝.
 Proof. by iIntros (?). Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index aa53de890..34b7029bf 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1525,7 +1525,7 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
-  | IPure :: ?pats => iIntro (?); iIntros_go pats startproof
+  | IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
   | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
   | IDrop :: ?pats => iIntro _; iIntros_go pats startproof
   | IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
-- 
GitLab