';' can be partially evaluated using Set Ltac Debug.

[palmskog]

Original report by Carst Tankink (Bitbucket: Carst, GitHub: Carst).

---

Investigate how useful this is when interfacing using Python (also with multiple goals).

[palmskog]

Original comment by Jason Gross (Bitbucket: jasongross9, ).

---

Oooh, this seems like it'd be really cool.

[palmskog]

Original comment by Carst Tankink (Bitbucket: Carst, GitHub: Carst).

---

Wow Issue-necro-ing!

Since then, there is a cooler option: prints of subgoals on arbitrary locations, combined with the PIDE library (for rebuilding a Proviola and/or giving feedback in an asynchronous interface): Enrico added the required code to Coq, the ';' tactical (and others) needs to be ported to support it. Bug the Coq devs and I'll see what I can do. ;)

[palmskog]

Original comment by Jason Gross (Bitbucket: jasongross9, ).

---

Oops. I was reporting a bug, and looked at the issues new since the last time I was here.

Is there an appropriate feature request on the bug tracker to bug the Coq devs about? I don't quite understand what it would mean for the ';' tactical (or any others) to support this.