Stream: Coq users

Topic: Printing of goal names


view this post on Zulip Joachim Breitner (Dec 04 2020 at 17:03):

Now that I can use the [name] { … } goal names, is there a way to tell Coq to actually print the goal names in the status windows (maybe instead of (1/6))?
(I found that I can see the goal names with Show Existentials, but that’s not ergonomic.)

view this post on Zulip Pierre-Marie Pédrot (Dec 04 2020 at 17:05):

There was a PR for that for CoqIDE recently.

view this post on Zulip Joachim Breitner (Dec 04 2020 at 17:17):

Ah, https://github.com/coq/coq/pull/13145. Thanks! Looking forward to that.


Last updated: Jan 29 2023 at 01:02 UTC