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

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.2.5+9.1.tbz
sha256=488520e2720cd0601a623be39ff87223d81ca1d2f81c77641f803fda21f3717e
sha512=146e43a6a9c516f4e7fe143d4fdf3e1e7ecdcd73ea5cc3e09b2886f68aa05210c016e905bf1596341faa0b55709ad530ef86212c92790b6dce6050a0a00e3325

doc/coq-lsp.serlib/Serlib/Ser_names/index.html

Module Serlib.Ser_namesSource

Sourcemodule Id : sig ... end
Sourcemodule Name : SerType.SJHC with type t = Names.Name.t
Sourcemodule DirPath : SerType.SJHC with type t = Names.DirPath.t
Sourcemodule DPmap : Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a Names.DPmap.t
Sourcemodule Label : SerType.SJHC with type t = Names.Label.t
Sourcemodule MBId : SerType.SJHC with type t = Names.MBId.t
Sourcemodule ModPath : SerType.SJHC with type t = Names.ModPath.t
Sourcemodule MPmap : Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a Names.MPmap.t
Sourcemodule KerName : SerType.SJHC with type t = Names.KerName.t
Sourcemodule KNmap : Ser_cMap.ExtS with type key = KerName.t and type 'a t = 'a Names.KNmap.t
Sourcemodule Constant : SerType.SJHC with type t = Names.Constant.t
Sourcemodule Cset_env : Ser_cSet.ExtS with type elt = Constant.t and type t = Names.Cset_env.t
Sourcemodule Cmap : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap.t
Sourcemodule Cmap_env : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap_env.t
Sourcemodule MutInd : SerType.SJHC with type t = Names.MutInd.t
Sourcemodule Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap.t
Sourcemodule Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap_env.t
Sourcemodule Indset_env : Ser_cSet.ExtS with type elt = Names.inductive and type t = Names.Indset_env.t
Sourcemodule Indmap_env : Ser_cMap.ExtS with type key = Names.inductive and type 'a t = 'a Names.Indmap_env.t
Sourcetype 'a tableKey = 'a Names.tableKey
Sourceval tableKey_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a tableKey
Sourceval sexp_of_tableKey : ('a -> Sexplib.Sexp.t) -> 'a tableKey -> Sexplib.Sexp.t
Sourcetype variable = Names.variable
Sourceval sexp_of_variable : variable -> Sexplib0.Sexp.t
Sourceval variable_of_sexp : Sexplib0.Sexp.t -> variable
Sourceval variable_to_yojson : variable -> Yojson.Safe.t
Sourceval hash_fold_variable : Ppx_hash_lib.Std.Hash.state -> variable -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_variable : variable -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_variable : variable -> variable -> int
Sourcetype inductive = Names.inductive
Sourceval sexp_of_inductive : inductive -> Sexplib0.Sexp.t
Sourceval inductive_of_sexp : Sexplib0.Sexp.t -> inductive
Sourceval inductive_to_yojson : inductive -> Yojson.Safe.t
Sourceval hash_fold_inductive : Ppx_hash_lib.Std.Hash.state -> inductive -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_inductive : inductive -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_inductive : inductive -> inductive -> int
Sourcetype constructor = Names.constructor
Sourceval sexp_of_constructor : constructor -> Sexplib0.Sexp.t
Sourceval constructor_of_sexp : Sexplib0.Sexp.t -> constructor
Sourceval constructor_to_yojson : constructor -> Yojson.Safe.t
Sourceval hash_fold_constructor : Ppx_hash_lib.Std.Hash.state -> constructor -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_constructor : constructor -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_constructor : constructor -> constructor -> int
Sourcemodule Projection : sig ... end
Sourcemodule GlobRef : SerType.SJHC with type t = Names.GlobRef.t
Sourcetype lident = Names.lident
Sourceval sexp_of_lident : lident -> Sexplib0.Sexp.t
Sourceval lident_of_sexp : Sexplib0.Sexp.t -> lident
Sourceval lident_to_yojson : lident -> Yojson.Safe.t
Sourceval hash_fold_lident : Ppx_hash_lib.Std.Hash.state -> lident -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_lident : lident -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_lident : lident -> lident -> int
Sourcetype lname = Names.lname
Sourceval sexp_of_lname : lname -> Sexplib0.Sexp.t
Sourceval lname_of_sexp : Sexplib0.Sexp.t -> lname
Sourceval lname_to_yojson : lname -> Yojson.Safe.t
Sourceval hash_fold_lname : Ppx_hash_lib.Std.Hash.state -> lname -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_lname : lname -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_lname : lname -> lname -> int
Sourcetype lstring = Names.lstring
Sourceval sexp_of_lstring : lstring -> Sexplib0.Sexp.t
Sourceval lstring_of_sexp : Sexplib0.Sexp.t -> lstring
Sourceval lstring_to_yojson : lstring -> Yojson.Safe.t
Sourceval hash_fold_lstring : Ppx_hash_lib.Std.Hash.state -> lstring -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_lstring : lstring -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_lstring : lstring -> lstring -> int