From a14f0fa3e21e3a2b55d090d1c99531dfbdced213 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 7 Apr 2020 08:42:35 -0500
Subject: [PATCH] Add support for naming forall intros

---
 tests/proofmode.v                 | 5 +++++
 theories/proofmode/ltac_tactics.v | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 01e0189a5..f27ba2444 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1097,6 +1097,7 @@ Ltac ltac_tactics.string_to_ident_hook ::=
   make_string_to_ident_hook ltac:(fun s => lazymatch s with
                                         | "HP2" => ident:(HP2)
                                         | "H" => ident:(H)
+                                        | "y" => ident:(y)
                                         | _ => fail 100 s
                                         end).
 
@@ -1111,6 +1112,10 @@ Proof.
   exact (Himpl HP2).
 Qed.
 
+Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) :
+  (∀ x : nat, Ψ x) ⊢ ∀ x : nat, Ψ x.
+Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
+
 Check "test_not_fresh".
 Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
   P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P2⌝.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 34b7029bf..b03db6a66 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1525,6 +1525,8 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
+  | IPure (IGallinaNamed ?s) :: ?pats => let i := string_to_ident s in
+                                         iIntro (i); 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
-- 
GitLab