Better integration of Derive in declare.ml + fix of #18951 - #19092

Merged

coqbot-app[bot] merged 6 commits into

rocq-prover:masterfrom

herbelin:master+fix18951-anomaly-derive-admitted

Aug 27, 2024

Commits on Jul 31, 2024

Derive: Code simplification wrt econstr.
herbelin
committed
bc812cc
Derive: better integration to declare.ml.
herbelin
committed
c11b5a5
Fixes #19234: preserve constraints across the individual components of Derive.
herbelin
committed
1806319
Exporting a definition attribute parser.
herbelin
committed
8be33f0
Preliminary support for attributes in Derive.
herbelin
committed
687bc06
Change log for #19092
herbelin
committed
3e37060