back to the main documentation page
The contents of pcoq windows a structured data. It is different from text in that it handled as tree structures carrying information about each command. This approach makes it easier to have nice mathematical notation and quicker systematic manipulation of commands. For instance, whenever you click in a non-empty window, a complete expression gets selected (you see this because its background becomes grey). This expression is one of the structures manipulated in the window. However, for users accustomed to manipulating text in word processors, it may be very confusing.
To help with this aspect, the pcoq system provides a specific menu, entitled Selection. The options provided in this menu are organized in two packages.
The first package provides the basic commands to move in the tree structure. Each node in this tree has siblings, a parent node, or children node. Some nodes, called Meta represent holes in the tree structure. One could also say that Meta nodes represent place-holder to fill in. As such they play a central role in the editing process and the Selection menu also provides quick ways to move from Meta node to Meta node.
The second package of navigating options provides more elaborate commands.