Skip to content
Post PR summary comment

RFC chore: do not import Tactic.Common in Mathlib #27783

Sign in to view logs

RFC chore: do not import Tactic.Common in Mathlib

RFC chore: do not import Tactic.Common in Mathlib #27783

Triggered via pull request October 31, 2024 16:32
@VierkantorVierkantor
synchronize #18498
unimport-Tactic.Common
Status Success
Total duration 48s
Artifacts –

PR_summary.yml

on: pull_request
build
41s
build
Fit to window
Zoom out
Zoom in