Bindings valid in all CtCoq windows (structure editing)

control-O Inserts a place-holder before the current selection.
control-B Moves the current selection to the left.
control-F Moves the current selection to the right.
escape control-U Moves the current selection towards the top.
escape control-D Moves the current selection on the first son.
escape f Moves the current selection to the first atomic tree on the left.
escape b Moves the current selection to the first atomic tree on the right.
escape p Moves the current selection to the first place-holder on the left.
escape n Moves the current selection to the first place-holder on the right.
escape m 1 Turns on the mode for automatic jump to the next place-holder.
escape m 0 Turns off the mode for automatic jump to the next place holder.
return In general, inserts a place holder after the current selection.
control-S Searches forward for the current search string.
control-R Searches backward for the current search string.
escape s Sets the search string and searches forward.
escape r Sets the search string and searches backward.
escape t Starts textual editing.
control-X m Shows or hides the template menu for structure guided editing.
control-X w Expands the current selection, to cancel the effect of ellision.
control-W Cut.
escape w Copy.
control-Y . Replace.
control-Y < Inserts before the current selection.
control-Y > Inserts after the current selection.
control-L Scrolls to the current selection.
control-X 4 f Loads a new file in another window.
control-X control-F Loads a new file.
control-X control-W Saves in a new file.
control-X control-S Saves the file.
control-X + Increments the print level.
control-X - Decrements the print level
control-X # 1 Sets the print level to 1
control-X # # Sets the print level to a very high value
control-Z > Scrolls one line up.
control-Z < Scrolls one line down.
control-X < Scrolls left.
control-X > Scrolls right.
escape g Goto line
control-X 2 Opens a second view on the same data.
control-V or
space 		Scrolls one page up.
escape v Scrolls one page down.
escape < Scrolls to the beginning.
escape > Scrolls to the end.
escape 2 or
escape 3 or
escape 4 or
escape 5 or
escape 6 or
escape 7 or
escape 8 or
escape 9 		Repeats the next command n times.
escape x Executes a function provided by the user.

Bindings valid in all CtCoq windows (text editing)

return New line.
escape Parses the text area.
back-space or
delete 		Deletes backward.
control-B Move left.
control-F Moves right.
control-P Moves up one line.
control-N Moves down one line.
control-K Removes the rest of the line.
control-E Goes to end of line.
control-A Goes to beginning of line.
control-D Delete one character forward.
bell Cancels text editing.
control-C g Do it.

Bindings valid in all Coq related windows

control-C s Searches for theorems proving the selected predicate (Coq's Search).
control-C c Type-checks the selected expression (Coq's Check).
control-C e Evaluates the selected expression (Coq's Eval).
control-C C Computes the selected expression (Coq's Compute).
control-C control-C e Eval, using the current goal's context.
control-C control-C c Check, using the current goal's context.
control-C control-C C Compute, using the current goal's context.
control-C p Prints the natural language proof of the selected name.
control-C t Toggle the Auto do it check box.
control-C g Do it.
control-C _ Discards the last command in Coq.
control-C k Aborts the current proof.

Bindings valid in all windows that contains premises

Windows of this kind include the State window, the Theorems window and the Library Fragment windows.
a Point and Apply.
e Point and Elim.
f Point and Auto.
r Point and Red.
w Point and Rewrite.
i Point and Injection.
g Point and Generalize.
l Point and Simpl.
m Point and Assumption (Proof by pointing)
! Duplicates the hypothesis.
z Generates a Specialize command.

Bindings valid in Theorems and Library Fragment windows

control-C d Creates a Library Fragment window.

Bindings valid only in State windows

Windows of this kind include the Commands windows and Definition windows.
control-C u Unfolds.
control-C w Clears hypotheses.
control-C ^ Creates a Coq Pattern command.
control-N Goes to next goal.
control-P Goes to previous goal.

Bindings valid in windows used for editing Coq commands

Windows of this kind include the Commands windows and Definition windows.
control-C a Executes all the commands in the window.
control-C d Opens a new multiple window.
control-C f Adds an Auto tactic to the current command.
control-C h Shows the goal on which the selected command was executed.
control-C q Prints the natural language explanation of the current proof.
control-C r Resets Coq to a state where the selected name is forgotten.
control-C v Insert a Qed. command.
control-C B Moves the current selection to an auxiliary window and file.