Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.

This addresses #529 in part.

TODO: Use _ prefix, but do that after !931 (merged) to avoid merge conflicts.