proofmode: make it possible for class_instances to use the proofmode

In ongoing work, I'd like to use the IPM to define instances in class_instances*.v. It turns out there is actually no reason this shouldn't work, we just need to remove some unused imports.

The only annoyance here is that everything just imports proofmode.tactics, so we need to make sure that this file does import the instances. To this end, the file defining the LTac tactics is renamed to ltac_tactics.v, and tactics.v just reexports that (and imports the instances).

coq_tactics.v still depends on modality_instances.v, which is not nice. It seems to be only needed to define MaybeIntoLaterNEnvs; maybe there is a better place for that?