Skip to content

[Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s)#39793

Closed
grunweg wants to merge 33 commits into
leanprover-community:masterfrom
grunweg:dupnamespace-stronger
Closed

[Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s)#39793
grunweg wants to merge 33 commits into
leanprover-community:masterfrom
grunweg:dupnamespace-stronger

Commits

Commits on May 29, 2026

Commits on May 30, 2026

Commits on Jun 2, 2026

Commits on Jun 3, 2026

Commits on Jun 4, 2026

Commits on Jun 5, 2026

Commits on Jun 8, 2026

Commits on Jun 9, 2026

Commits on Jun 17, 2026

Commits on Jul 1, 2026