• General tactics
• Domain specific tactics
• Generic tactics
• Hypothesis iteration in Ltac and Ltac2