Skip to content
Backport

chore: final module system fixes and refinements for initial Mathlib porting #14289

Sign in to view logs

chore: final module system fixes and refinements for initial Mathlib porting

chore: final module system fixes and refinements for initial Mathlib porting #14289

Triggered via pull request October 24, 2025 16:14
@KhaKha
closed #10869
Status Success
Total duration 13s
Artifacts –

backport.yml

on: pull_request_target
Backport
5s
Backport
Fit to window
Zoom out
Zoom in