Refine
Extraargs
Extratactics
Eauto
Class_tactics
Tauto
Eqdecide