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

[herbelin]

The PR better integrates Derive to declare.ml. It supports CInfo.t, Info.t and uses the declare_entry execution path. As a consequence, Derive now supports rather directly:

• universe polymorphism
• implicit arguments

By eventually exporting DefAttributes so that g_derive.mlg can use it, it could also support all standard attributes of definitions.

The PR relies on the support of Admitted for multiple statement goals in #19090 to support Admitted on Derive, thus also fixing #18951.

A full merge of the End_derive path in the End_regular path will be possible when:

• the flow of treatment of universes will be swapped as in A unique execution path for the treatement of universes in declare.ml rfcs#89 that is when the universes will be treated in declare_possibly_mutual_definitions instead of in prepare_proof and close_proof
• different opacities on different components of a multi-statement will be possible, as in a variant of Experiment the addition of sealed/defined attributes #19029 where sealedness is stored in CInfo rather than in Info
• declare_possibly_mutual_definitions will support dependent goals (as declare_possibly_mutual_parameters now does)

Eventually, we can also imagine providing for free n-ary forms of Derive in the following style:

Derive f with g with h
  SuchThat T As H with U As I with V as J
  SuchThat W As K with X As L with Y as M.`

Fixes #18951

• Added / updated test-suite.
• Added changelog.
• Add support for general declaration attributes

Depends on:

• Towards a more uniform API for declare.ml (part declaring mutual statements) #18795
• [Subsumed] Add optional type annotation to Derive #19087 (to be able to do tests)
• Make CSet extensible on our side, and adding CSet.List.union. #19075 (in a minor way)
• Add support for Admitted on multiple statements #19090
• Use multiple statements to implement interactive fixpoints #19091 (to be able to use the same execution path as interactive fixpoints)

[coqbot-app]

🔴 CI failure at commit fc7954d without any failure in the test-suite

✔️ Corresponding job for the base commit 43402d4 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-rupicola

• You can also pass me a specific list of targets to minimize as arguments.

[herbelin]

CI happy.

Note that the test for #18951 will be in #19295.

[ppedrot]

Looks reasonable to me.

[ppedrot]

@SkySkimmer if you have no additional comment on the current state, I can proceed to merge.

[ppedrot]

No answer from @SkySkimmer so @coqbot merge now