package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Flags : sig ... end
module Warning : sig ... end
module Require : sig ... end
type t = private {
  1. coqlib : string;
  2. coqcorelib : string;
  3. ocamlpath : string option;
  4. vo_load_path : Loadpath.vo_path list;
    (*

    List of -R / -Q flags passed to Coq, usually theories we depend on

    *)
  5. ml_include_path : string list;
    (*

    List of paths to look for Coq plugins, deprecated in favor of findlib

    *)
  6. require_libs : Require.t list;
    (*

    Modules to preload, usually Coq.Init.Prelude

    *)
  7. flags : Flags.t;
    (*

    Coq-specific flags

    *)
  8. warnings : Warning.t list;
  9. kind : string;
    (*

    How the workspace was built

    *)
  10. debug : bool;
    (*

    Enable backtraces

    *)
}
val inject_requires : extra_requires:Require.t list -> t -> t

Inject some requires

val compare : t -> t -> int

compare

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 default : debug:bool -> cmdline:CmdLine.t -> 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct