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: Mar 29 2024 at 13:01 UTC