This is the on-line help for CtCoq. It is still incomplete, but you can get quick information on the following topics:

• Description of the windows of CtCoq
• Mouse bindings in all windows
• Key bindings in all windows
• Editing commands and formulas
• Extending notations
• Executing and undoing commands
• Interaction with the file system
• Proof-by-Pointing
• "drag and drop" rewrite
• Proof explanation
• Adding you own tactics
• Context help

We also intend to have a few tutorials, that guide you through sample sessions:

• A simple arithmetic proof
• Using script management
• All about Proof-by-pointing

To order CtCoq or to have more information on the system, click here