Avoid `Local Ltac` and `Local Tactic Notation`

There appears to be no way to call such tactics outside of the module, making debugging very difficult.

For Local Ltac, I think this is a Coq bug, see https://github.com/coq/coq/issues/17884

For Local Tactic Notation, I think it's inherently broken since Tactic Notation extends the grammar.