Joachim Breitner (Dec 04 2020 at 17:03): 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.)
Pierre-Marie Pédrot (Dec 04 2020 at 17:05):There was a PR for that for CoqIDE recently.
Joachim Breitner (Dec 04 2020 at 17:17):Ah, https://github.com/coq/coq/pull/13145. Thanks! Looking forward to that.
Last updated: Apr 20 2024 at 07:01 UTC