Skip to content

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection)#837

Merged
andrew-appel merged 1 commit intoPrincetonUniversity:masterfrom
SkySkimmer:fix-apply-nreal
Sep 22, 2025
Merged

Adapt to rocq-prover/rocq#21063 (fixed apply auto-projecting from record with letin projection)#837
andrew-appel merged 1 commit intoPrincetonUniversity:masterfrom
SkySkimmer:fix-apply-nreal