5.5 Loadpath
There are currently two loadpaths in Coq. A loadpath where seeking Coq files (extensions .v or .vo or .vi) and one where seeking Objective Caml files. The default loadpath contains the directory ``.'' denoting the current directory, so there also commands to print and change the current working directory.5.5.1 Pwd.
This command displays the current working directory.5.5.2 Cd string.
This command changes the current directory according to string which can be any valid path.Variants:
-
Cd.
Is equivalent to Pwd.
5.5.3 AddPath string.
This command adds the path string to the current Coq loadpath.5.5.4 DelPath string.
This command removes the path string from the current Coq loadpath.5.5.5 Print LoadPath.
This command displays the current Coq loadpath.5.5.6 Add ML Path string.
This command adds the path string to the current Objective Caml loadpath (see the command Declare ML Module in the section 5.4).5.5.7 Print ML Path string.
This command displays the current Objective Caml loadpath. This command makes sense only under the bytecode version of oqtop, i.e. not using -opt or -full options (see the command Declare ML Module in the section 5.4).5.5.8 Locate File string.
This command displays the location of file string in the current loadpath. Typically, string is a .cmo or .vo or .v file.5.5.9 Locate Library ident.
This command displays the location of the Coq module ident in the current loadpath. Is is equivalent to Locate File "ident.vo".5.5.10 Locate ident.
This command displays the full name of the identifier ident and consequently the Coq module in which it is defined.