package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (32)

Authors

Maintainers

E

e@x80.org

Sources

coq-lsp-0.2.0.8.20.tbz

sha256=bcb9a4c3219aed47ffbfd7c8ea7a2f374140d8cdb76079927548f49c7e3576a9

sha512=945c0010b4952e41055cb7e35175d400e5c126dc340dd1c0ab53321605cd0d9539af6693a794cb81a9dec0385d0880d4417dae923b6d19c9b62913766a185d8c

doc/coq-lsp.fleche/Fleche/Doc/Env/index.html

Module `Doc.Env`Source

Enviroment external to the document, this includes for now the init Coq state and the workspace, which are used to build the first state of the document, usually by importing the prelude and other libs implicitly.

Sourcetype t = private {

init : Coq.State.t;
workspace : Coq.Workspace.t;
files : Coq.Files.t;

}

Source

val make : 
  init:Coq.State.t ->
  workspace:Coq.Workspace.t ->
  files:Coq.Files.t ->
  t

Sourceval inject_requires : extra_requires:Coq.Workspace.Require.t list -> t -> t