add quick_exact tactic from Jason

and clean up a bit