Stream: Coq devs & plugin devs

Topic: Replacement for Goal.V82.abstract_type


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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: Jun 14 2024 at 19:02 UTC