https://charlesaverill.github.io/ctpe/
I’ve been using Coq for a little longer than a year now. One of the things that left me very apprehensive about learning more about the system was the (in my opinion) poor availability of simple explanations of tactics. We have the official tactic index, which is, for lack of a better word, scary for a new Coq user. Then there are a few intro to tactics lists, but they focus a lot on the tactics that I was able to figure out on my own. So I decided to write yet another list of tactics that I think get used a lot but don’t get enough attention, especially their alternate forms.
I’m updating this in my free time so not a whole lot of constant development. Next big category I’d like to add are the e-tactics (In hindsight, I had way too much trouble understanding them for how complex their usage actually is - likely a me problem).