diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2fd6728b5b85ffbb444c724d9d09b5f62ffbcf38..f7c535f5bbe636331c03574cfcf792d765ac4dc7 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 aaef16cd02a3347ea28ca9b6ebc50aae0dec6838..95b27c49140d64956953f83097142fb7b1f2988d 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.