Adrian Cucoș (Jun 12 2021 at 12:56): 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).
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: Apr 19 2024 at 09:01 UTC