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.3.8.18.tbz

sha256=f574f3323a00eab3c158ae70dfd88fbbe90c8c86f95e0f175570266d5b401b14

sha512=2bd46a630a21306ccd62469f29fa60bb43d96c62d8236abafd15f9c2cd904070d92ec566263d1b8f151698914a6d740e5f6adcfb020c338e90a0b23a4457bc16

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