Commit 2024-07-09 11:47 bcbcbff8

fix: make the allowed unused tactics extensible (#14557) This PR allows to change the tactics that the unused tactic linter ignores. The main use-case is allowing done at the end of proofs, which is very useful for teaching purposes. See for instance this Zulip thread.