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.

assigned to @msammler

mentioned in merge request !389 (closed)

Result of discussion with Robbert:

• The current naming scheme makes sense and it is preferable to have such a consistent naming scheme compared to having all kinds of tactics that all follow the same pattern but have different names.
• Splitting the MRs was a mistake and the other MR should be integrated into this one.
• (e)feed should be renamed to (e)feed_core
• by flag should be removed from efeed
• (e)feed revert should be named (e)feed generalize
• feed destruct and efeed destruct should be documented to be the same as destruct and edestruct, but have them for consistency
• add a comment that efeed generalize is exploit from CompCert
• add a comment that efeed inversion allows not just identifiers, unlike inversion

added 1 commit

• 30220cd7 - Add the feed generalize, efeed generalize, efeed inversion, and efeed destruct tactics

Compare with previous version

changed title from Improve documentation of feed and efeed tactics to Refactor and improve documentation of feed and efeed tactics

changed the description

added 1 commit

• c0225349 - Refactor feed and add the feed generalize, efeed generalize, efeed inversion,...

Compare with previous version

added 1 commit

• 94212f09 - Refactor feed and add the feed generalize, efeed generalize, efeed inversion,...

Compare with previous version

add a comment that efeed generalize is exploit from CompCert

That sounds to be a key tactic then, might be good to have a usage example at least for this one.

added 1 commit

• ff6c6c18 - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

added 19 commits

• ff6c6c18...02fd8ca3 - 18 commits from branch master
• d0eca127 - Refactor feed and add the feed generalize, efeed generalize, efeed inversion,...

Compare with previous version

added 1 commit

• 7662c360 - Refactor feed and add the feed generalize, efeed generalize, efeed inversion,...

Compare with previous version

added 1 commit

• 603bef84 - Refactor feed and add the feed generalize, efeed generalize, efeed inversion,...

Compare with previous version