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.2.0.8.19.tbz
sha256=01ffedbd55ae00526fe1dda890e3c15a883bfda8388c8d292121ee722db46360
sha512=b5d92146c27b5c432a3f92c9ae8ff69c4dc62709f394743ca2d43ab93ae3af64b08bb17ea5923c0fbe0a333de127de574c548ec3c8df81dbe3e11f485abc3216

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

Module Serlib.Ser_tactypesSource

Sourcemodule CAst = Ser_cAst
Sourcemodule Names = Ser_names
Sourcemodule Namegen = Ser_namegen
Sourcemodule EConstr = Ser_eConstr
Sourcetype 'a intro_pattern_action_expr = 'a Tactypes.intro_pattern_action_expr =
  1. | IntroWildcard
  2. | IntroOrAndPattern of 'a or_and_intro_pattern_expr
  3. | IntroInjection of 'a intro_pattern_expr CAst.t list
  4. | IntroApplyOn of 'a CAst.t * 'a intro_pattern_expr CAst.t
  5. | IntroRewrite of bool
Sourceand 'a intro_pattern_expr = 'a Tactypes.intro_pattern_expr =
  1. | IntroForthcoming of bool
  2. | IntroNaming of Namegen.intro_pattern_naming_expr
  3. | IntroAction of 'a intro_pattern_action_expr
Sourceand 'a or_and_intro_pattern_expr = 'a Tactypes.or_and_intro_pattern_expr =
  1. | IntroOrPattern of 'a intro_pattern_expr CAst.t list list
  2. | IntroAndPattern of 'a intro_pattern_expr CAst.t list
Sourceval intro_pattern_action_expr_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a intro_pattern_action_expr
Sourceval intro_pattern_expr_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a intro_pattern_expr
Sourceval or_and_intro_pattern_expr_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_and_intro_pattern_expr
Sourceval sexp_of_intro_pattern_action_expr : 'a. ('a -> Sexplib0.Sexp.t) -> 'a intro_pattern_action_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_intro_pattern_expr : 'a. ('a -> Sexplib0.Sexp.t) -> 'a intro_pattern_expr -> Sexplib0.Sexp.t
Sourceval sexp_of_or_and_intro_pattern_expr : 'a. ('a -> Sexplib0.Sexp.t) -> 'a or_and_intro_pattern_expr -> Sexplib0.Sexp.t
Sourceval intro_pattern_action_expr_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a intro_pattern_action_expr -> Yojson.Safe.t
Sourceval intro_pattern_expr_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a intro_pattern_expr -> Yojson.Safe.t
Sourceval or_and_intro_pattern_expr_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a or_and_intro_pattern_expr -> Yojson.Safe.t
Sourceval hash_fold_intro_pattern_action_expr : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a intro_pattern_action_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fold_intro_pattern_expr : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a intro_pattern_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fold_or_and_intro_pattern_expr : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a or_and_intro_pattern_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_intro_pattern_action_expr : 'a. ('a -> 'a -> int) -> 'a intro_pattern_action_expr -> 'a intro_pattern_action_expr -> int
Sourceval compare_intro_pattern_expr : 'a. ('a -> 'a -> int) -> 'a intro_pattern_expr -> 'a intro_pattern_expr -> int
Sourceval compare_or_and_intro_pattern_expr : 'a. ('a -> 'a -> int) -> 'a or_and_intro_pattern_expr -> 'a or_and_intro_pattern_expr -> int
Sourcetype quantified_hypothesis = Tactypes.quantified_hypothesis =
  1. | AnonHyp of int
  2. | NamedHyp of Names.lident
Sourceval quantified_hypothesis_of_sexp : Sexplib0.Sexp.t -> quantified_hypothesis
Sourceval sexp_of_quantified_hypothesis : quantified_hypothesis -> Sexplib0.Sexp.t
Sourceval quantified_hypothesis_to_yojson : quantified_hypothesis -> Yojson.Safe.t
Sourceval hash_fold_quantified_hypothesis : Ppx_hash_lib.Std.Hash.state -> quantified_hypothesis -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_quantified_hypothesis : quantified_hypothesis -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_quantified_hypothesis : quantified_hypothesis -> quantified_hypothesis -> int
Sourcetype 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
Sourceval explicit_bindings_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a explicit_bindings
Sourceval sexp_of_explicit_bindings : 'a. ('a -> Sexplib0.Sexp.t) -> 'a explicit_bindings -> Sexplib0.Sexp.t
Sourceval explicit_bindings_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a explicit_bindings -> Yojson.Safe.t
Sourceval hash_fold_explicit_bindings : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a explicit_bindings -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_explicit_bindings : 'a. ('a -> 'a -> int) -> 'a explicit_bindings -> 'a explicit_bindings -> int
Sourcetype 'a bindings = 'a Tactypes.bindings =
  1. | ImplicitBindings of 'a list
  2. | ExplicitBindings of 'a explicit_bindings
  3. | NoBindings
Sourceval bindings_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a bindings
Sourceval sexp_of_bindings : 'a. ('a -> Sexplib0.Sexp.t) -> 'a bindings -> Sexplib0.Sexp.t
Sourceval bindings_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a bindings -> Yojson.Safe.t
Sourceval hash_fold_bindings : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a bindings -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_bindings : 'a. ('a -> 'a -> int) -> 'a bindings -> 'a bindings -> int
Sourcetype 'a with_bindings = 'a * 'a bindings
Sourceval with_bindings_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_bindings
Sourceval sexp_of_with_bindings : 'a. ('a -> Sexplib0.Sexp.t) -> 'a with_bindings -> Sexplib0.Sexp.t
Sourceval with_bindings_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a with_bindings -> Yojson.Safe.t
Sourceval hash_fold_with_bindings : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a with_bindings -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_with_bindings : 'a. ('a -> 'a -> int) -> 'a with_bindings -> 'a with_bindings -> int
Sourcemodule DO : sig ... end
Sourcemodule B : sig ... end
Sourcetype 'a delayed_open = 'a B.t
Sourceval delayed_open_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a delayed_open
Sourceval sexp_of_delayed_open : 'a. ('a -> Sexplib0.Sexp.t) -> 'a delayed_open -> Sexplib0.Sexp.t
Sourceval delayed_open_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a delayed_open -> Yojson.Safe.t
Sourceval hash_fold_delayed_open : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a delayed_open -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_delayed_open : 'a. ('a -> 'a -> int) -> 'a delayed_open -> 'a delayed_open -> int
Sourcetype delayed_open_constr = EConstr.constr delayed_open
Sourceval delayed_open_constr_of_sexp : Sexplib0.Sexp.t -> delayed_open_constr
Sourceval sexp_of_delayed_open_constr : delayed_open_constr -> Sexplib0.Sexp.t
Sourceval delayed_open_constr_to_yojson : delayed_open_constr -> Yojson.Safe.t
Sourceval hash_fold_delayed_open_constr : Ppx_hash_lib.Std.Hash.state -> delayed_open_constr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_delayed_open_constr : delayed_open_constr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_delayed_open_constr : delayed_open_constr -> delayed_open_constr -> int
Sourcetype delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
Sourceval delayed_open_constr_with_bindings_of_sexp : Sexplib0.Sexp.t -> delayed_open_constr_with_bindings
Sourceval sexp_of_delayed_open_constr_with_bindings : delayed_open_constr_with_bindings -> Sexplib0.Sexp.t
Sourceval delayed_open_constr_with_bindings_to_yojson : delayed_open_constr_with_bindings -> Yojson.Safe.t
Sourceval _ : Yojson.Safe.t -> delayed_open_constr_with_bindings Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_delayed_open_constr_with_bindings : Ppx_hash_lib.Std.Hash.state -> delayed_open_constr_with_bindings -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_delayed_open_constr_with_bindings : delayed_open_constr_with_bindings -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_delayed_open_constr_with_bindings : delayed_open_constr_with_bindings -> delayed_open_constr_with_bindings -> int