Skip to content

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

Merged
samuelgruetter merged 1 commit into
mit-plv:rv32ifrom
SkySkimmer:gene-eqs-vars
May 4, 2026
Merged

Adapt to rocq-prover/rocq#22001 (dependent induction less useless generalizations)#48
samuelgruetter merged 1 commit into
mit-plv:rv32ifrom
SkySkimmer:gene-eqs-vars

Adapt to rocq-prover/rocq#22001 (dependent induction less useless gen…

7d158b4
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
build (master, coq libcoq-core-ocaml-dev, ppa:jgross-h/coq-master-daily)
succeeded May 4, 2026 in 1h 0m 13s