Emilio Jesús Gallego Arias

cc: https://github.com/ocaml/ocaml/issues/5797 https://github.com/ocaml/ocaml/issues/6338

> @ejgallego What should be done to resolve this? That requires developer discussion; usually you would expect types that can be saved to disk to implement a `Serializable.S` interface that...

There have been improvements on this recently, we should check if this is solved.

Something this plan needs is a maintainer of the sub-system that will collaborate on reviewing / merging PRs, IMHO the most hairy ones have been done and the upcoming ones...

Very good point, there is a great mess in that aspect; my current tree does improve the situation with `imp` quite a bit IMO, but of course there still is...

See new entry added @jashug > - in particular make sure that declare_manual_implicits is called in a central place for all proofs.

Ok, with the submission of #10316 the first part of the refactoring is complete; once we arrive there we can proceed to the second phase which is the big unification...

Main thing I'm working on now is on the path for delayed proofs, from the upper layer point of view, #10337 makes the "opaque QED, proof delayed" call explicit, however...

We have made quite a bit of progress! The main issues now indeed do seem: - reduce code duplication, improve API for dependent proofs [todo: link to Matthieu slides] -...

> * reduce code duplication The following paths to save a constant are in a sense duplicated: - `Proof_global.close_proof` - `DeclareDef.prepare_definition/declare_definition` - `Lemmas.finish_proved/save_remaining_recthms` - `Record.declare_*` - `DeclareObls`, etc... A good...