Stream: Coq users

Topic: How can I print the current goal?

Ignat Insarov (Jun 20 2021 at 17:51):

Is there an Ltac command that prints the current goal _(or other parts of state)_ to the response window?

Théo Winterhalter (Jun 20 2021 at 18:05):

idtac can print stuff that you give to it as argument, including terms.
So you could write

lazymatch goal with
| |- ?g => idtac g
end.

Ignat Insarov (Jun 20 2021 at 18:16):

Thanks!

Last updated: Jan 29 2023 at 05:03 UTC