Quick Help

Basic Navigation

Button	Key binding	Action
	`F8`	Toggles the goal panel.
	`Alt`+`↓`/`↑` or `Alt`+`N`/`P`	Move through the proof.
	`Alt`+`Enter` or `Ctrl`+`Enter` (`⌘` on Mac)	Run (or go back) to the current point.
	`Ctrl`+	Hover executed statements to peek at the proof state after each step.
	`Esc`	Interrupt a currently executing statement.
		Completely restart Coq, re-initializing document and libraries.

Button	Key binding	Action
		Open the scratchpad for editing. (This icon is located in the landing page and on the splash screen.)
	`Ctrl`+`S`	Save file in the browser's local storage (with the last name provided, or `untitled.v`).
	`Ctrl`+`Shift`+`S`	Save file as (prompts for local file name), download to disk, or share.
	`Ctrl`+`Alt`+`S`	Save file to disk (using the browser's Save dialog, or preset destination if such is configured in your browser).
	`Ctrl`+`O`	Open file (prompts for local file name from list, supports tab completion).

On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.