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

Fix the check_porting bug when there are name collisions

fd9b4f2
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
build
succeeded Aug 12, 2026 in 31s