Commit 2026-04-25 07:57 a78e0492

View on Github →

chore: clean up group (#38491) This PR cleans up the source for the group tactic slightly. It

  • prefixes the internal lemmas with _ to hide them from autocomplete (and renames their additivized versions correctly)
  • inlines the two internal aux_group tactics, which are used exactly once and are not extended (this has the nice side effect of removing them from the tactic documentation page)
  • causes group to fail if it makes no progress (this helps hint be less noisy)
  • removes meta from an import

Estimated changes