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.
Edited by Robbert Krebbers
This addresses #529 in part.
TODO: Use _ prefix, but do that after !931 (merged) to avoid merge conflicts.