coq-serapi
coq-serapi copied to clipboard
[upstream] Automating the registration of serializers for generic arguments
trafficstars
As witnessed by #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.