Check awaiting-mathlib label

fix: make `register_try?_tactic` auxiliary definitions internal #18206

Sign in to view logs

Triggered via pull request December 8, 2025 05:34

kim-em

opened #11547

kim-em:fix-register-try-tactic-internal-names

Status Success

Total duration 7s

Artifacts –

awaiting-mathlib.yml

on: pull_request

check-awaiting-mathlib