Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics

theories/tactics.v

@@ -499,7+499,7 @@
 (** Given [H : A_1 → ... → A_n → B] (where each [A_i] is non-dependent), the
 tactic [feed tac H tac_by] creates a subgoal for each [A_i] and calls [tac p]
 with the generated proof [p] of [B]. *)
 Tactic Notation "feed" tactic(tac) constr(H) :=
   let rec go H :=
   let T := type of H in
   lazymatch eval hnf in T with
@@ -516,7+516,7 @@
 
 (** The tactic [efeed tac H] is similar to [feed], but it also instantiates
 dependent premises of [H] with evars. *)
 Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) :=
   let rec go H :=
   let T := type of H in
   lazymatch eval hnf in T with
@@ -548,7+548,7 @@
 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. *)