Coq.Workspace
module Flags : sig ... end
module Warning : sig ... end
module Require : sig ... end
type t = private {
coqlib : string;
coqcorelib : string;
ocamlpath : string option;
vo_load_path : Loadpath.vo_path list;
List of -R / -Q flags passed to Coq, usually theories we depend on
*)ml_include_path : string list;
List of paths to look for Coq plugins, deprecated in favor of findlib
*)require_libs : Require.t list;
Modules to preload, usually Coq.Init.Prelude
*)flags : Flags.t;
Coq-specific flags
*)warnings : Warning.t list;
kind : string;
How the workspace was built
*)debug : bool;
Enable backtraces
*)}
val hash : t -> int
hash
val describe : t -> string * string
user message, debug extra data
val describe_guess : (t, string) Result.t -> string * string
module CmdLine : sig ... end
val guess :
token:Limits.Token.t ->
debug:bool ->
cmdline:CmdLine.t ->
dir:string ->
(t, string) Result.t
val apply : uri:Lang.LUri.File.t -> t -> unit
apply libname w
will prepare Coq for a new file libname
on workspace w
val dirpath_of_uri : uri:Lang.LUri.File.t -> Names.DirPath.t