Skip to content

Fix: handle local Rocq name collisions in check-porting.py - #622

Merged
lzy0505 merged 1 commit into
leanprover-community:masterfrom
lzy0505:zliu/fix-porting-name-collusion
Aug 12, 2026
Merged

Fix: handle local Rocq name collisions in check-porting.py#622
lzy0505 merged 1 commit into
leanprover-community:masterfrom
lzy0505:zliu/fix-porting-name-collusion

Commits

Commits on Aug 12, 2026