General tactics

• TacticExts small tactics that are widely useful

Domain specific tactics

• RingTactics tactics for reasoning about ring structures
• InTac tactic to prove the inclusion of list

Generic tactics

• GenericTactics a few tactics letting the user define its domain specific tactics

Hypothesis iteration in Ltac and Ltac2

• generic iterators over hypotheses in a goal in Ltac and Ltac2