Added select and select_revert tactics

As discussed with @robbertkrebbers open points:

• Names of the tactics (What are the names in Mtac? @janno )
• Changelog entry?

The name in Mtac2 is select: https://github.com/Mtac2/Mtac2/blob/master/theories/tactics/Tactics.v#L737

The tactic is a bit different, it returns the name of the hypothesis, instead of calling a continuation (which would backtrack in case of multiple matches).

Do you think returning the name would be a better option here as well?

added 1 commit

• 087d31c2 - Added select and select_revert tactics

Compare with previous version

resolved all threads

I think this MR is ready. @jung any objections to merge?

marked the checklist item Names of the tactics (What are the names in Mtac? @janno ) as completed

marked the checklist item Changelog entry? as completed

added 1 commit

• bc565b4e - Added select and select_revert tactics

Compare with previous version

added 1 commit

• f9beb585 - Added select and select_revert tactics

Compare with previous version

added 1 commit

• 18113ce2 - Added select and select_revert tactics

Compare with previous version

added 1 commit

• e25a9be2 - Added select and select_revert tactics

Compare with previous version

resolved all threads

LGTM.

added 13 commits

• e25a9be2...1d9cb6c8 - 12 commits from branch master
• 23984e60 - Added select and select_revert tactics

Compare with previous version

added 1 commit

• 92213810 - Added select and select_revert tactics

Compare with previous version