package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install 

dune-project
 Dependency

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

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.1.9.8.17.tbz
sha256=a89d86ed8b19d09bf3a06acbed690ae2859a7343d9faa03537c76cd492371651
sha512=edae491b284d5ab586c82cea4003a5b477f41ab25a4659431d4bc8caaee39b62de03b64d088ab8c528416210f88f73d4dfe5efbd32b22c70b75c9d18999c1e00

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

Module Doc.EnvSource

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 {
  1. init : Coq.State.t;
  2. workspace : Coq.Workspace.t;
  3. files : Coq.Files.t;
}
Sourceval 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