[upstream] Automating the registration of serializers for generic arguments

[ejgallego]

As witnessed by ejgallego/coq-serapi#68, we have a very important problem with the current situation of generic arguments in Coq. As of today, we need to add manually the serializers, which is cumbersome, and worse, won't fail until we find a generic argument we cannot handle.

Ideally we should add some support in Coq to notify SerAPI that a new generic argument has been defined, then SerAPI could look up its internal serializer table and register it.

Even better, it would be good if coqpp could generate some kind of boilerplate thus that we could be spared from writing the serializers manually, but this may have to wait for ppx_serlib to be ready tho.

List of times we got bitten by this problem: (started in May 2024, many more missing)

• [serlib] [ltac2] Fix wrong piercing creating havoc. coq-serapi#413
• [serlib] Fix wrong piercing of Ltac2 AST + test case #821