- [[clear-tactic|clear]] : Remove unused hypotheses from the local context. The `clear` tactic removes one or more hypotheses from the local context. It is primarily used to prevent clutter. - Suggested comment style: clear \_hQ -- `Q` is unneeded. **Note:** that the underbar prefix to hQ denotes that the hypotheses is unneeded and that clear removes it from the infoview. --- Author: [[dducoff]] Posted Date: 2026-06-25