To understand what Command window, State window, Theorems window, etc mean, you should have a look at the section describing all the windows of CtCoq. In this page, the mouse bindings are grouped following the windows in which they are valid. A more thematic organization can follow the following main ideas: text and structure editing, proof by pointing and point and shoot, drag and drop rewrite, script management, and natural language presentation of proofs.

Mouse Bindings

Text Editing Mode

For more information on the text editing mode see the page on editing.

LeftSet Cursor

Mouse bindings common to all windows

More information on these bindings is also given in the section on editing.

LeftSet Current Selection
<Shift> LeftCopy to the X buffer
<Ctrl> Left Scroll Window (when reaching the border).

Mouse bindings in the Command windows

MiddleLocal Copy-paste
<Shift> MiddleParse the X buffer and replace

Mouse bindings common to the State, Theorems and Library Fragment windows

MiddleCopy-paste to the Command window
RightProof by Pointing
<Ctrl> rightMenu for Proof by Pointing

Mouse bindings for the State and Theorems windows

<Shift> MiddlePop up display menu
<Shift> RightPop up selections menu

Mouse bindings in the State windows

<Ctrl>LeftDrag and drop rewrite

Mouse bindings in the Library Fragment windows

<Shift>MiddleParse the X buffer and replace