Module Envars
This file provides a high-level interface to the environment variables needed by Coq to run (such as coqlib). The values of these variables may come from different sources (shell environment variables, command line options, options set at the time Coq was build).
val expand_path_macros : warn:(string -> unit) -> string -> stringexpand_path_macros warn ssubstitutes environment variables in a string by their values. This function also takes care of substituting path of the form '~X' by an absolute path. Usewarnas a message displayer.
val home : warn:(string -> unit) -> stringhome warnreturns the root of the user directory, depending on the OS. This information is usually stored in the $HOME environment variable on POSIX shells. If no such variable exists, then other common names are tried (HOMEDRIVE, HOMEPATH, USERPROFILE). If all of them fail,warnis called.
val coqroot : stringcoqrootis the path tocoqbin. The following value only makes sense when executables are running from source tree (e.g. during build or in local mode).
val coqpath : string listcoqpathis the standard path to coq. Notice that coqpath is stored in reverse order, since that is the order it gets added to the search path.