Skip to content

Make dependent elimination compatible with Set Mangle Names - #734

Open
thomas-lamiaux wants to merge 1 commit into
rocq-prover:mainfrom
thomas-lamiaux:fix-mangle-names-733
Open

Make dependent elimination compatible with Set Mangle Names#734
thomas-lamiaux wants to merge 1 commit into
rocq-prover:mainfrom
thomas-lamiaux:fix-mangle-names-733

Commits

Commits on Jul 25, 2026