From db4424f201978980725f802df3a994898889a0d2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Feb 2018 20:16:17 +0100
Subject: [PATCH] Accept spec pattern ASTs in `with` syntax.

As requested by @jtassaro.
---
 theories/proofmode/tactics.v | 6 +++---
 theories/tests/proofmode.v   | 7 +++++++
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2fd6728b5..f7c535f5b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -455,9 +455,9 @@ Local Tactic Notation "iIntro" :=
   end.
 
 (** * Specialize *)
-Record iTrm {X As} :=
-  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
-Arguments ITrm {_ _} _ _ _.
+Record iTrm {X As S} :=
+  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
+Arguments ITrm {_ _ _} _ _ _.
 
 Notation "( H $! x1 .. xn )" :=
   (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index aaef16cd0..95b27c491 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -362,4 +362,11 @@ Proof. iIntros "H". iFrame "H". auto. Qed.
 
 Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". auto. Qed.
+
+Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R.
+Proof.
+  iIntros "? HQ H".
+  iMatchHyp (fun H _ =>
+    iApply ("H" with [spec_patterns.SIdent H; spec_patterns.SIdent "HQ"])).
+Qed.
 End tests.
-- 
GitLab