Towards a more uniform API for declare.ml (part declaring mutual statements)

[herbelin]

The purpose of this PR is to present some uniformity in the API of declare.ml so that it is clearer to compare the different functions. It should not change the semantics.

Depends on #18742 and #18743 (merged).

It has an impact on the exact API though with the following API changes:

• function renamings

  • declare_mutually_recursive -> declare_mutual_definition (+ label rec_declaration -> bodies), consistently with declare_definition
  • start_with_initialization -> start_definition
  • start_mutual_with_initialization -> start_mutual_definition (+ label init_term -> bodies)

• other labels renaming

  • in add_definition: term -> body, and opaque made mandatory
  • in add_mutual_definitions: argument (cinfo,bodies,obls) -> labels cinfo and bodies + obls kept as unnamed argument

• TODO, pending question: mutual_definition or mutual_definitions?

Overlays (due to opaque made mandatory)

• Adapt to Coq PR #18795 (more uniform API for declare.ml) MetaCoq/metacoq#1083
• Adapt to Coq PR #18795 (more uniform API for declare.ml) mattam82/Coq-Equations#599

[ejgallego]

The most conservative would be mutual definitions since it would preserve the old name add_mutual_definitions, so I'm leaning for it.

Sounds good @herbelin , I have no strong opinion, if we find a better name we can change it later of course.

[herbelin]

Adopting the plural form then.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 18795-herbelin-master+uniform-API-declare.ml.sh