Arpan Agrawal (Jul 14 2023 at 18:57): Arpan Agrawal (Jul 14 2023 at 18:57):I'm working on porting a plugin from Coq 8.9 to Coq 8.16, and noticed that this commit inlines the Goal.V82.abstract_type function in the funind plugin. Is there a different function in the new API that does the same thing or is it not recommended to represent goals as types?
Thanks!
Karl Palmskog (Jul 14 2023 at 19:16):general suggestion for best practices in porting plugins: look at the diffs between tags for a maintained plugin, such as: https://github.com/coq-community/aac-tactics
For example, this shows the diff between the v8.9.0 and the v8.10.0 tag: https://github.com/coq-community/aac-tactics/compare/v8.9.0..v8.10.0
Gaëtan Gilbert (Jul 14 2023 at 20:09):Is there a different function in the new API that does the same thing or is it not recommended to represent goals as types?
There's no new API. I don't know about recommended, but you're free to copy the function into your plugin if you find it useful (assuming license compatibility I guess? IANAL)
look at the diffs between tags for a maintained plugin
funind counts no?
Last updated: Oct 13 2024 at 01:02 UTC