diff --git a/theories/tactics.v b/theories/tactics.v
index d4c143a6faf0c86a147470ceaac4025c744c7d4e..ad120b58a9ca15f04df7dd1f8df307db0daf2892 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -548,15 +548,30 @@ Tactic Notation "feed" "specialize" hyp(H) :=
 Tactic Notation "efeed" "specialize" hyp(H) :=
   efeed H using (fun p => specialize p).
 
+Tactic Notation "feed" "generalize" constr(H) :=
+  feed (fun p => let H':=fresh in pose proof p as H'; generalize H') H.
+Tactic Notation "efeed" "generalize" constr(H) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; generalize H').
+
 Tactic Notation "feed" "inversion" constr(H) :=
   feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H.
+Tactic Notation "efeed" "inversion" constr(H) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; inversion H').
+
 Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP) H.
+Tactic Notation "efeed" "inversion" constr(H) "as" simple_intropattern(IP) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP).
 
 Tactic Notation "feed" "destruct" constr(H) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H') H.
+Tactic Notation "efeed" "destruct" constr(H) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; destruct H').
+
 Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
+Tactic Notation "efeed" "destruct" constr(H) "as" simple_intropattern(IP) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP).
 
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)