Refactor and improve documentation of feed and efeed tactics

This MR is based on !389 (closed).

Discussion from !389 (comment 82974) :

The documentation does not even mention the by part of this tactic. Also, efeed tac H (which is what the documentation uses in the first line) is not the correct syntax for this tactic. Maybe feed should also be adjusted to be written feed H using tac? Actually 'using' is a strange verb here, it sounds like tac is involved in the feeding, but that's not the case. Is to a keyword already, i.e., can we use efeed H to tac? Or into?

See also the discussion here: !389 (comment 82750)

@robbertkrebbers Please feel free to update this MR as you see fit.

theories/tactics.v

@@ -497,8 +497,13 @@ Tactic Notation "iter" tactic(tac) tactic(l) :=
   match l with ?x :: ?l => tac x || go l end in go l.
 
 (** 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 [feed tac H] creates a subgoal for each [A_i] and calls [tac p]
+with the generated proof [p] of [B].
+
+For example, given [H : P → Q → R], [feed (fun p => pose proof p) H] creates the
+subgoals [P] and [Q] and then executes [pose proof Hfeed] where [Hfeed : R],
+which adds [R] to the context of the original goal.
+ *)
 Tactic Notation "feed" tactic(tac) constr(H) :=
   let rec go H :=
   let T := type of H in
@@ -515,7 +520,12 @@ Tactic Notation "feed" tactic(tac) constr(H) :=
   end in go H.
 
 (** The tactic [efeed tac H] is similar to [feed], but it also instantiates
-dependent premises of [H] with evars. *)
+dependent premises of [H] with evars.
+
+For example, given [H : ∀ x y, P x → Q y → R x y], [efeed H using (fun p => pose proof p)]
+creates evars [?x] and [?y] for [x] and [y] and subgoals [P ?x] and [Q ?y] and
+then executes [pose proof Hfeed] where [Hfeed : R ?x ?y], which adds [R ?x ?y]
+to the context of the original goal. *)
 Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) :=
   let rec go H :=
   let T := type of H in
@@ -548,15 +558,30 @@ Tactic Notation "feed" "specialize" hyp(H) :=
 Tactic Notation "efeed" "specialize" hyp(H) :=
   efeed H using (fun p => specialize p).
 
+Tactic Notation "feed" "revert" constr(H) :=
+  feed (fun p => let H':=fresh in pose proof p as H'; revert H') H.
+Tactic Notation "efeed" "revert" constr(H) :=
+  efeed H using (fun p => let H':=fresh in pose proof p as H'; revert 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. *)