Stream: SerAPI

Topic: VernacExtend and SerAPI


view this post on Zulip Adrian Cucoș (Jun 12 2021 at 12:56):

I was reading the FAQ for SerApi and I came across the mentioning of internalization and pretyping VernacExtend types. However, I could not find an explanation of what that means or how it could be achieved (in terms of Ltac2).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2021 at 20:44):

Hi @Adrian Cucoș ! Indeed there is an open issue already as to automate this, for now, one needs to write a wrapper for every plugin in serlib/plugins and sertop/sertop_loader.ml; please open an issue to add ltac2 support [with some test cases please] and we should be able to fix it quickly.


Last updated: Feb 06 2023 at 07:03 UTC