5.6 States and Reset
5.6.1 Reset ident.
This command removes all the objects in the environment since ident was introduced, including ident. ident may be the name of a defined or declared object as well as the name of a section. One cannot reset over the name of a module or of an object inside a module.Error messages:
- cannot reset to a nonexistent object
5.6.2 Save State ident.
Saves the current state of the development (mainly the defined objects) such that one can go back at this point if necessary.Variants:
-
Save State ident string.
Associates to the state of name ident the string string as a comment.
5.6.3 Print States.
Prints the names of the currently saved states with the associated comment. The state Initial is automatically built by the system and can not be removed.5.6.4 Restore State ident.
Restores the set of known objects in the state ident.Variants:
-
Reset Initial.
Is equivalent to Restore State Initial and goes back to the initial state (like after the command coqtop).
5.6.5 Remove State ident.
Remove the state ident from the states list.5.6.6 Write States string.
Writes the current list of states into a UNIX file string.coq for use in a further session. This file can be given as the inputstate argument of the commands coqtop and coqc. A command Restore State ident is necessary afterwards to choose explicitly which state to use (the default is to use the last saved state).Variants:
- Write States ident The suffix .coq is implicit, and the state is saved in the current directory (see X).