Is there a canonical way to find out what section variables were used by a proof? Best I can think of is by getting the type of the lemma before closing the section, then closing the section, then comparing to find which new binders exist after closing the section, and comparing those to the types of all section variables declared in the section. This seems kind of hacky and relies on a bunch of syntax heuristics though, is there a better way?

Yes, there is a better way but it is ML-only for the API. We can expose such API in SerAPI / coq-lsp tho, please open a ticket

The way is what the section closing mechanism does

Created issues in the coq-lsp and coq-serapi repos. But, proof general seems to be able to do this (the `coq-insert-suggested-dependency`

command), it doesn't use the ML api does it?

Oh, it may use the `Suggest Proof Using`

command

So that command could also work for you, but I'm unsure how structured it is. Basically what I was proposing is implementing that command

in serapi / coq-lsp

as the functionality is there

you can do `About my_lemma`

and it will say `my_lemma uses section variables foo bar baz`

since 8.17 https://github.com/coq/coq/pull/16208

Went through the PG source a bit, it does indeed use Suggest Proof Using (it was easier to find once I knew what I was looking for. I would use the `About`

command, but I work with older versions of Coq. I'll try Proof Using for now, and when the functionality gets added to coq-lsp or serapi I can use that too. Thanks!

Last updated: Jun 13 2024 at 19:02 UTC