diff --git a/theories/tactics.v b/theories/tactics.v
index 4045a47e1bb78af132c09c114592162ad9f40b59..d715c743faa051a9e92a69daa465df7073b63bba 100644
--- a/theories/tactics.v
+++ b/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).