[declare] Grand unification of the proof save path.

We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.

In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.

The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .

There are still some TODOs, that will be addressed in subsequent PRs:

- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]

List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:

- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"

0 files changed, 0 insertions, 0 deletions