Stream: Coq devs & plugin devs

Topic: definitions.rst


view this post on Zulip Fabian Kunze (Nov 26 2020 at 10:50):

is the definitions.rst file in docs/sphinx/language/core autogenerated or do I need to update it if changing something mentioned there?

view this post on Zulip Enrico Tassi (Nov 26 2020 at 10:57):

It is not autogenerated but there is a tool to double check that is you change the grammar or a command then it is in sync with the one in the doc.
But you let the doc maintainers check it I believe.

view this post on Zulip Enrico Tassi (Nov 26 2020 at 10:58):

You can also open a PR without updating the doc, and amend after


Last updated: Oct 15 2021 at 20:02 UTC