The default key bindings of CoqIDE are often problematic because they conflict with the window manager. Moreover, the default bindings are not efficient at all: the most useful action requires pressing a combination of 3 keys... Fortunately, it is straightforward to update the bindings.

Configuring the alternative set of bindings

(For Coq version >= 8.4 only)

Close all running instances of CoqIDE, then download and install the modified configuration file as follows:

The alternative set of bindings

After you copied the modified configuration file, the new bindings are as follows:

Execute until cursor


Execute backward one step


Execute forward one step


Execute to the end


Run make


Reach next error


Interrupt execution


Reset execution


How to manually modify the bindings

You can edit the binding files coqide.keys yourself. (It is located in ~/.config/coq/ or C:\Program Files\Coq\config\). To modify a binding, edit the corresponding line by removing the semi-column at the beginning of the line and changing the shortcut. Example:


;(gtk_accel_path "/Navigation/_Go to/" "<CTRL><ALT>Right")


(gtk_accel_path "/Navigation/_Go to/" "F5")

Other tips for Coqide

Copy-pasting: to copy a piece of text from proof context or from the error message pannel, you cannot use the CTRL+C key binding, however the key binding CTRL+INSERT does work.

Focus: CoqIDE can be slowed down a lot by the Focus command. Do not use it. Instead, use "admit" to skip subgoals until you can view the one that you are interested in.

Cocorico: Configuration of CoqIDE (last edited 26-01-2013 17:55:59 by oumix)