Is there an Ltac command that prints the current goal _(or other parts of state)_ to the response window?
idtac
can print stuff that you give to it as argument, including terms.
So you could write
lazymatch goal with
| |- ?g => idtac g
end.
Thanks!
Last updated: Jan 29 2023 at 05:03 UTC