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: Sep 23 2023 at 14:01 UTC