Use [notypeclasses refine] for all proofmode tactics
As done ad-hoc for two tactics in 5249f4c4 to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.
As done ad-hoc for two tactics in 5249f4c4 to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.