Accept spec pattern ASTs in `with` syntax.

As requested by @jtassaro.

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).

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.