If I make a mistake (such as "cannot unify") in a proof and :CoqToCursor to a later line, the error message doesn't display anywhere. Is there a way to show errors, like the "Errors" tab in CoqIDE?
A workaround is to step through line-by-line in order to see them, but I think there's probably a better way.
And thank you so much for this tool, it's joy to use Coq in Vim.
If I make a mistake (such as "cannot unify") in a proof and
:CoqToCursorto a later line, the error message doesn't display anywhere. Is there a way to show errors, like the "Errors" tab in CoqIDE? A workaround is to step through line-by-line in order to see them, but I think there's probably a better way.And thank you so much for this tool, it's joy to use Coq in Vim.