package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val parse_env_line : string -> (string * string) option
val with_ic : string -> (in_channel -> 'a) -> 'b
val getenv_from_file : string -> string
val system_getenv : string -> string
val getenv_else : string -> (unit -> string) -> string
val use_suffix : string -> string -> string

Add a local installation suffix (unless the suffix is itself absolute in which case the prefix does not matter)

val canonical_path_name : string -> string
val coqbin : string
val coqroot : string

The following only makes sense when executables are running from source tree (e.g. during build or in local mode).

val check_file_else : dir:string -> file:string -> (unit -> string) -> string

check_file_else ~dir ~file oth checks if file exists in the installation directory dir given relatively to coqroot, which maybe has been relocated. If the check fails, then oth () is evaluated. Using file system equality seems well enough for this heuristic