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