Taking a fun tactic implemented in class, and making it public for further refinement and generalization, and for implementation in other frameworks.
The original course with more information is here.
To compile the Ltac version, you will need StructTact.