5.3 Loading files

5.3 Loading files

Coq offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded files are ASCII files containing sequences of commands for Coq's toplevel. This kind of file is called a script for Coq. The standard (and default) extension of Coq's script files is .v.

5.3.1 Load ident.

This command loads the file named ident.v, searching successively in each of the directories specified in the loadpath. (see section 5.5)


Variants:
  1. Load string.
    Loads the file denoted by the string string, where string is any complete filename. Then the ~ and .. abbreviations are allowed as well as shell variables. If no extension is specified, Coq will use the default extension .v
  2. Load Verbose ident., Load Verbose string
    Display, while loading, the answers of Coq to each command (including tactics) contained in the loaded file
    See also: section 5.8.3



Error messages:
  1. Can't find file ident on loadpath


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.0.2.html at 8/10/98