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 (38)

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.18.tbz
sha256=99514bcbf82318b9ff857656f4ec1f87bb46f1c699a4f1e9fb06f5fcdd8d8839
sha512=fa4593a2ae416e554869a879da5d35a1d33efa5cc8743f77c05373875ecea267019989dec600d5e880d909aea97ce7f6990ac59e58aabce358e3693b0764bef8

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