Generalize (e)feed pose proof to intro patterns

This appears a simple oversight, since pose proof takes an intro pattern anyway; feed inversion and feed destruct already take intro patterns, and I've been using the generalized efeed pose proof for a while.

theories/tactics.v

@@ -427,12 +427,12 @@ Tactic Notation "efeed" constr(H) "using" tactic3(tac) :=
 
 (** The following variants of [pose proof], [specialize], [inversion], and
 [destruct], use the [feed] tactic before invoking the actual tactic. *)
-Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+Tactic Notation "feed" "pose" "proof" constr(H) "as" simple_intropattern(H') :=
   feed (fun p => pose proof p as H') H.
 Tactic Notation "feed" "pose" "proof" constr(H) :=
   feed (fun p => pose proof p) H.
 
-Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+Tactic Notation "efeed" "pose" "proof" constr(H) "as" simple_intropattern(H') :=
   efeed H using (fun p => pose proof p as H').
 Tactic Notation "efeed" "pose" "proof" constr(H) :=
   efeed H using (fun p => pose proof p).