I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way to issue an arbitrary Gallina query, via the prompt?
That is: Both VSCoq and Proof General provide specific commands to issue frequently used Gallina queries from the command prompt/minibuffer (e.g. VSCoq’s
Coq: Prompt Check for Gallina’s
Check). But often I want to issue a less-common Gallina query (e.g.
Eval), and either no editor command/keybinding is provided, or I haven’t memorised it yet. Proof General provides an excellent catch-all command for this situation: “Issue command” (
C-c C-v), which lets the user type an arbitrary Gallina query in the minibuffer. Is there some equivalent in VSCoq?
Of course, there is a fallback option of typing the query in the proof script, stepping forward, then stepping back and deleting the line afterwards. But it would be nice to avoid these extra steps.
(To be technically precise: by “query”, I mean the kinds of Gallina command that Proof General classes as state-preserving —