Adapt to Coq PR #19301: unify the syntax of definition and theorem#869

Open

herbelin wants to merge 2 commits intoejgallego:mainfrom herbelin:main+adapt-coq-pr19301-ceps42-unify-definition-theorem

+12-20

Commits on Oct 23, 2024

Adapt to Coq PR #19301
herbelin
committed

Commits on Oct 27, 2024

Adapt to Coq PR #19301, continued
herbelin
committed