Add the feed generalizef, efeed generalize, efeed inversion, and efeed destruct tactics

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