Adapt to https://github.com/rocq-prover/rocq/pull/21947#855
Open
proux01 wants to merge 1 commit intoPrincetonUniversity:masterfrom
Open
Adapt to https://github.com/rocq-prover/rocq/pull/21947#855proux01 wants to merge 1 commit intoPrincetonUniversity:masterfrom
proux01 wants to merge 1 commit intoPrincetonUniversity:masterfrom
