Keybindings - siegebell/vscoq GitHub Wiki

You can modify vscode keybindings by pressing F1 and typing "Preferences: Open Keyboard Shortcuts". You may have to reload your workspace for the changes to take effect.

• Proof General
• CoqIDE

Proof General

You can manually add your own keybindings for the rest of emacs support, or download an extension that provides some keybindings for you: e.g. vscode-emacs or emacs. However, not all bindings may be available to assign; more than two chord keys (e.g. ctrl+c ctrl+a ctrl+b) are not currently supported by vscode (#6966).

{ "key": "ctrl+c ctrl+n", "command": "extension.coq.stepForward", "when": "editorTextFocus && editorLangId == 'coq'"},
{ "key": "ctrl+c ctrl+u", "command": "extension.coq.stepBackward", "when": "editorTextFocus && editorLangId == 'coq'" },
{ "key": "ctrl+c ctrl+enter", "command": "extension.coq.interpretToPoint", "when": "editorTextFocus && editorLangId == 'coq'" },
{ "key": "ctrl+c ctrl+b", "command": "extension.coq.interpretToEnd", "when": "editorTextFocus && editorLangId == 'coq'" },
{ "key": "ctrl+c ctrl+r", "command": "extension.coq.reset", "when": "editorTextFocus && editorLangId == 'coq'" },
{ "key": "ctrl+c ctrl+c", "command": "extension.coq.interrupt", "when": "editorTextFocus && editorLangId == 'coq'" },
{ "key": "ctrl+c ctrl+n", "command": "extension.coq.stepForward", "when": "resourceScheme==coq-view"},
{ "key": "ctrl+c ctrl+u", "command": "extension.coq.stepBackward", "when": "resourceScheme==coq-view" },
{ "key": "ctrl+c ctrl+enter", "command": "extension.coq.interpretToPoint", "when": "resourceScheme==coq-view" },
{ "key": "ctrl+c ctrl+b", "command": "extension.coq.interpretToEnd", "when": "resourceScheme==coq-view" },
{ "key": "ctrl+c ctrl+c", "command": "extension.coq.interrupt", "when": "resourceScheme==coq-view" }

CoqIDE (default)

{"key": "ctrl+alt+home", "command": "extension.coq.reset", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+`", "command": "extension.coq.interrupt", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+break", "command": "extension.coq.interrupt", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+down", "command": "extension.coq.stepForward", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+up", "command": "extension.coq.stepBackward", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+right", "command": "extension.coq.interpretToPoint", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+end", "command": "extension.coq.interpretToEnd", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+.", "command": "extension.coq.moveCursorToFocus", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+a", "command": "extension.coq.query.about", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+k", "command": "extension.coq.query.searchAbout", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+l", "command": "extension.coq.query.locate", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+c", "command": "extension.coq.query.check", "when": "editorTextFocus && editorLangId == coq"},
{"key": "ctrl+alt+p", "command": "extension.coq.query.print", "when": "editorTextFocus && editorLangId == coq"},
{"key": "shift+alt+i", "command": "extension.coq.display.toggle.implicitArguments", "when": "editorTextFocus && editorLangId == coq"},
{"key": "shift+alt+c", "command": "extension.coq.display.toggle.coercions", "when": "editorTextFocus && editorLangId == coq"},
{"key": "shift+alt+n", "command": "extension.coq.display.toggle.notations", "when": "editorTextFocus && editorLangId == coq"},

{"key": "ctrl+alt+home", "command": "extension.coq.reset", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+`", "command": "extension.coq.interrupt", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+break", "command": "extension.coq.interrupt", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+down", "command": "extension.coq.stepForward", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+up", "command": "extension.coq.stepBackward", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+right", "command": "extension.coq.interpretToPoint", "when": "resourceScheme==coq-view"},
{"key": "ctrl+alt+end", "command": "extension.coq.interpretToEnd", "when": "resourceScheme==coq-view"},
{"key": "shift+alt+i", "command": "extension.coq.display.toggle.implicitArguments", "when": "resourceScheme==coq-view"},
{"key": "shift+alt+c", "command": "extension.coq.display.toggle.coercions", "when": "resourceScheme==coq-view"},
{"key": "shift+alt+n", "command": "extension.coq.display.toggle.notations", "when": "resourceScheme==coq-view"}