Skip to content
Jonathan Leivent edited this page Aug 18, 2020 · 14 revisions

General tactics

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

Clone this wiki locally