Adapt to rocq-prover/rocq#22001 (dependent induction less useless generalizations)#48

samuelgruetter merged 1 commit into

mit-plv:rv32imit-plv/kami:rv32ifrom

SkySkimmer:gene-eqs-varsSkySkimmer/kami:gene-eqs-varsCopy head branch name to clipboard