STM: code refactoring

This is mainly shuffling code around and removing internal
refs that are not needed anymore.
Show: do print the goals
vernac_classifier: VernacDeclareTacticDefinition does not alter the parser