Add examples and comments for all tactics that don't have them yet

[awalterschulze]

The contributing guidelines has a new preference:

Tactics unlike proofs, definitions, etc. don't have any types. This means they lack some documentation and type checking. For this reason, we prefer that new tactics come with:
  - some comments above that describe the tactic.
  - some examples below that use the tactic.

https://github.com/awalterschulze/regex-reexamined-coq/blob/master/CONTRIBUTING.md#tactics

There is still lots of tactics that have been committed that don't have examples or comments from before this new preference.

Search the codebase for Ltac and find these occurrences, add examples and comments as described. Here is an example of how to add examples and comments.
https://github.com/awalterschulze/regex-reexamined-coq/blob/master/src/CoqStock/WreckIt.v