Skip to content

Do not store recursive trees anymore in inductive blocks.#21901

Open
ppedrot wants to merge 2 commits intorocq-prover:masterfrom
ppedrot:rm-inductive-recarg-from-declarations
Open

Do not store recursive trees anymore in inductive blocks.#21901
ppedrot wants to merge 2 commits intorocq-prover:masterfrom
ppedrot:rm-inductive-recarg-from-declarations

Commits

Commits on Apr 15, 2026