This MR is based on !389 (closed).
Discussion from !389 (comment 82974) :
The documentation does not even mention the
bypart 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
feedshould also be adjusted to be written
feed H using tac? Actually 'using' is a strange verb here, it sounds like
tacis involved in the feeding, but that's not the case. Is
toa keyword already, i.e., can we use
efeed H to tac? Or
See also the discussion here: !389 (comment 82750)
@robbertkrebbers Please feel free to update this MR as you see fit.