package coq-lsp

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

Install

Dune Dependency

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

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.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223

doc/serlib_ssr/Serlib_ssr/Ser_ssrast/index.html

Module Serlib_ssr.Ser_ssrastSource

module Loc = Serlib.Ser_loc
module Names = Serlib.Ser_names
module Locus = Serlib.Ser_locus
module Constrexpr = Serlib.Ser_constrexpr
module Genintern = Serlib.Ser_genintern
module Geninterp = Serlib.Ser_geninterp
Sourcemodule Ssrmatching_plugin : sig ... end
Sourcemodule Ltac_plugin : sig ... end
Sourceval ssrtermkind_of_sexp : Sexplib0.Sexp.t -> ssrtermkind
Sourceval sexp_of_ssrtermkind : ssrtermkind -> Sexplib0.Sexp.t
Sourceval ssrtermkind_to_yojson : ssrtermkind -> Yojson.Safe.t
Sourceval ssrtermkind_of_yojson : Yojson.Safe.t -> ssrtermkind Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrtermkind : Ppx_hash_lib.Std.Hash.state -> ssrtermkind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrtermkind : ssrtermkind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrtermkind : ssrtermkind -> ssrtermkind -> int
Sourcemodule Proofview : sig ... end
Sourcetype ssrhyp = Ssreflect_plugin__Ssrast.ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
Sourceval ssrhyp_of_sexp : Sexplib0.Sexp.t -> ssrhyp
Sourceval sexp_of_ssrhyp : ssrhyp -> Sexplib0.Sexp.t
Sourceval ssrhyp_to_yojson : ssrhyp -> Yojson.Safe.t
Sourceval ssrhyp_of_yojson : Yojson.Safe.t -> ssrhyp Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhyp : Ppx_hash_lib.Std.Hash.state -> ssrhyp -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrhyp : ssrhyp -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrhyp : ssrhyp -> ssrhyp -> int
Sourcetype ssrhyp_or_id = Ssreflect_plugin__Ssrast.ssrhyp_or_id =
  1. | Hyp of ssrhyp
  2. | Id of ssrhyp
Sourceval ssrhyp_or_id_of_sexp : Sexplib0.Sexp.t -> ssrhyp_or_id
Sourceval sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Sexplib0.Sexp.t
Sourceval ssrhyp_or_id_to_yojson : ssrhyp_or_id -> Yojson.Safe.t
Sourceval ssrhyp_or_id_of_yojson : Yojson.Safe.t -> ssrhyp_or_id Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhyp_or_id : Ppx_hash_lib.Std.Hash.state -> ssrhyp_or_id -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrhyp_or_id : ssrhyp_or_id -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrhyp_or_id : ssrhyp_or_id -> ssrhyp_or_id -> int
Sourcetype ssrhyps = ssrhyp list
Sourceval ssrhyps_of_sexp : Sexplib0.Sexp.t -> ssrhyps
Sourceval sexp_of_ssrhyps : ssrhyps -> Sexplib0.Sexp.t
Sourceval ssrhyps_to_yojson : ssrhyps -> Yojson.Safe.t
Sourceval ssrhyps_of_yojson : Yojson.Safe.t -> ssrhyps Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhyps : Ppx_hash_lib.Std.Hash.state -> ssrhyps -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrhyps : ssrhyps -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrhyps : ssrhyps -> ssrhyps -> int
Sourceval ssrdir_of_sexp : Sexplib0.Sexp.t -> ssrdir
Sourceval sexp_of_ssrdir : ssrdir -> Sexplib0.Sexp.t
Sourceval ssrdir_to_yojson : ssrdir -> Yojson.Safe.t
Sourceval ssrdir_of_yojson : Yojson.Safe.t -> ssrdir Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrdir : Ppx_hash_lib.Std.Hash.state -> ssrdir -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrdir : ssrdir -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrdir : ssrdir -> ssrdir -> int
Sourcetype ssrsimpl = Ssreflect_plugin__Ssrast.ssrsimpl =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
Sourceval ssrsimpl_of_sexp : Sexplib0.Sexp.t -> ssrsimpl
Sourceval sexp_of_ssrsimpl : ssrsimpl -> Sexplib0.Sexp.t
Sourceval ssrsimpl_to_yojson : ssrsimpl -> Yojson.Safe.t
Sourceval ssrsimpl_of_yojson : Yojson.Safe.t -> ssrsimpl Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrsimpl : Ppx_hash_lib.Std.Hash.state -> ssrsimpl -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrsimpl : ssrsimpl -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrsimpl : ssrsimpl -> ssrsimpl -> int
Sourcetype ssrmmod = Ssreflect_plugin__Ssrast.ssrmmod =
  1. | May
  2. | Must
  3. | Once
Sourceval ssrmmod_of_sexp : Sexplib0.Sexp.t -> ssrmmod
Sourceval sexp_of_ssrmmod : ssrmmod -> Sexplib0.Sexp.t
Sourceval ssrmmod_to_yojson : ssrmmod -> Yojson.Safe.t
Sourceval ssrmmod_of_yojson : Yojson.Safe.t -> ssrmmod Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrmmod : Ppx_hash_lib.Std.Hash.state -> ssrmmod -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrmmod : ssrmmod -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrmmod : ssrmmod -> ssrmmod -> int
Sourcetype ssrmult = int * ssrmmod
Sourceval ssrmult_of_sexp : Sexplib0.Sexp.t -> ssrmult
Sourceval sexp_of_ssrmult : ssrmult -> Sexplib0.Sexp.t
Sourceval ssrmult_to_yojson : ssrmult -> Yojson.Safe.t
Sourceval ssrmult_of_yojson : Yojson.Safe.t -> ssrmult Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrmult : Ppx_hash_lib.Std.Hash.state -> ssrmult -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrmult : ssrmult -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrmult : ssrmult -> ssrmult -> int
Sourcetype ssrocc = (bool * int list) option
Sourceval ssrocc_of_sexp : Sexplib0.Sexp.t -> ssrocc
Sourceval sexp_of_ssrocc : ssrocc -> Sexplib0.Sexp.t
Sourceval ssrocc_to_yojson : ssrocc -> Yojson.Safe.t
Sourceval ssrocc_of_yojson : Yojson.Safe.t -> ssrocc Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrocc : Ppx_hash_lib.Std.Hash.state -> ssrocc -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrocc : ssrocc -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrocc : ssrocc -> ssrocc -> int
Sourcetype ssrindex = int Locus.or_var
Sourceval ssrindex_of_sexp : Sexplib0.Sexp.t -> ssrindex
Sourceval sexp_of_ssrindex : ssrindex -> Sexplib0.Sexp.t
Sourceval ssrindex_to_yojson : ssrindex -> Yojson.Safe.t
Sourceval ssrindex_of_yojson : Yojson.Safe.t -> ssrindex Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrindex : Ppx_hash_lib.Std.Hash.state -> ssrindex -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrindex : ssrindex -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrindex : ssrindex -> ssrindex -> int
Sourcetype ssrclear = ssrhyps
Sourceval ssrclear_of_sexp : Sexplib0.Sexp.t -> ssrclear
Sourceval sexp_of_ssrclear : ssrclear -> Sexplib0.Sexp.t
Sourceval ssrclear_to_yojson : ssrclear -> Yojson.Safe.t
Sourceval ssrclear_of_yojson : Yojson.Safe.t -> ssrclear Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrclear : Ppx_hash_lib.Std.Hash.state -> ssrclear -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrclear : ssrclear -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrclear : ssrclear -> ssrclear -> int
Sourcetype ssrdocc = ssrclear option * ssrocc
Sourceval ssrdocc_of_sexp : Sexplib0.Sexp.t -> ssrdocc
Sourceval sexp_of_ssrdocc : ssrdocc -> Sexplib0.Sexp.t
Sourceval ssrdocc_to_yojson : ssrdocc -> Yojson.Safe.t
Sourceval ssrdocc_of_yojson : Yojson.Safe.t -> ssrdocc Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrdocc : Ppx_hash_lib.Std.Hash.state -> ssrdocc -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrdocc : ssrdocc -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrdocc : ssrdocc -> ssrdocc -> int
Sourceval ssrterm_of_sexp : Sexplib0.Sexp.t -> ssrterm
Sourceval sexp_of_ssrterm : ssrterm -> Sexplib0.Sexp.t
Sourceval ssrterm_to_yojson : ssrterm -> Yojson.Safe.t
Sourceval ssrterm_of_yojson : Yojson.Safe.t -> ssrterm Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrterm : Ppx_hash_lib.Std.Hash.state -> ssrterm -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrterm : ssrterm -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrterm : ssrterm -> ssrterm -> int
Sourcetype ast_glob_env = Ssreflect_plugin__Ssrast.ast_glob_env = {
  1. ast_ltacvars : Names.Id.Set.t;
  2. ast_extra : Genintern.Store.t;
  3. ast_intern_sign : Genintern.intern_variable_status;
}
Sourceval ast_glob_env_of_sexp : Sexplib0.Sexp.t -> ast_glob_env
Sourceval sexp_of_ast_glob_env : ast_glob_env -> Sexplib0.Sexp.t
Sourceval ast_glob_env_to_yojson : ast_glob_env -> Yojson.Safe.t
Sourceval ast_glob_env_of_yojson : Yojson.Safe.t -> ast_glob_env Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ast_glob_env : Ppx_hash_lib.Std.Hash.state -> ast_glob_env -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ast_glob_env : ast_glob_env -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ast_glob_env : ast_glob_env -> ast_glob_env -> int
Sourcetype ast_closure_term = Ssreflect_plugin__Ssrast.ast_closure_term = {
  1. body : Constrexpr.constr_expr;
  2. glob_env : ast_glob_env option;
  3. interp_env : Geninterp.interp_sign option;
  4. annotation : [ `At | `DoubleParens | `Parens | `None ];
}
Sourceval ast_closure_term_of_sexp : Sexplib0.Sexp.t -> ast_closure_term
Sourceval sexp_of_ast_closure_term : ast_closure_term -> Sexplib0.Sexp.t
Sourceval ast_closure_term_to_yojson : ast_closure_term -> Yojson.Safe.t
Sourceval ast_closure_term_of_yojson : Yojson.Safe.t -> ast_closure_term Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ast_closure_term : Ppx_hash_lib.Std.Hash.state -> ast_closure_term -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ast_closure_term : ast_closure_term -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ast_closure_term : ast_closure_term -> ast_closure_term -> int
Sourcetype ssrview = ast_closure_term list
Sourceval ssrview_of_sexp : Sexplib0.Sexp.t -> ssrview
Sourceval sexp_of_ssrview : ssrview -> Sexplib0.Sexp.t
Sourceval ssrview_to_yojson : ssrview -> Yojson.Safe.t
Sourceval ssrview_of_yojson : Yojson.Safe.t -> ssrview Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrview : Ppx_hash_lib.Std.Hash.state -> ssrview -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrview : ssrview -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrview : ssrview -> ssrview -> int
Sourcetype anon_kind = Ssreflect_plugin__Ssrast.anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
Sourceval anon_kind_of_sexp : Sexplib0.Sexp.t -> anon_kind
Sourceval sexp_of_anon_kind : anon_kind -> Sexplib0.Sexp.t
Sourceval anon_kind_to_yojson : anon_kind -> Yojson.Safe.t
Sourceval anon_kind_of_yojson : Yojson.Safe.t -> anon_kind Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_anon_kind : Ppx_hash_lib.Std.Hash.state -> anon_kind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_anon_kind : anon_kind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_anon_kind : anon_kind -> anon_kind -> int
Sourcetype id_block = Ssreflect_plugin__Ssrast.id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
Sourceval id_block_of_sexp : Sexplib0.Sexp.t -> id_block
Sourceval sexp_of_id_block : id_block -> Sexplib0.Sexp.t
Sourceval id_block_to_yojson : id_block -> Yojson.Safe.t
Sourceval id_block_of_yojson : Yojson.Safe.t -> id_block Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_id_block : Ppx_hash_lib.Std.Hash.state -> id_block -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_id_block : id_block -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_id_block : id_block -> id_block -> int
Sourcetype ssripat = Ssreflect_plugin__Ssrast.ssripat =
  1. | IPatNoop
  2. | IPatId of Names.Id.t
  3. | IPatAnon of anon_kind
  4. | IPatDispatch of ssripatss_or_block
  5. | IPatCase of ssripatss_or_block
  6. | IPatInj of ssripatss
  7. | IPatRewrite of ssrocc * ssrdir
  8. | IPatView of ssrview
  9. | IPatClear of ssrclear
  10. | IPatSimpl of ssrsimpl
  11. | IPatAbstractVars of Names.Id.t list
  12. | IPatFastNondep
Sourceand ssripats = ssripat list
Sourceand ssripatss = ssripats list
Sourceand ssripatss_or_block = Ssreflect_plugin__Ssrast.ssripatss_or_block =
  1. | Block of id_block
  2. | Regular of ssripats list
Sourceval ssripat_of_sexp : Sexplib0__.Sexp.t -> ssripat
Sourceval ssripats_of_sexp : Sexplib0__.Sexp.t -> ssripats
Sourceval ssripatss_of_sexp : Sexplib0.Sexp.t -> ssripatss
Sourceval ssripatss_or_block_of_sexp : Sexplib0.Sexp.t -> ssripatss_or_block
Sourceval sexp_of_ssripat : ssripat -> Sexplib0__.Sexp.t
Sourceval sexp_of_ssripats : ssripats -> Sexplib0__.Sexp.t
Sourceval sexp_of_ssripatss : ssripatss -> Sexplib0.Sexp.t
Sourceval sexp_of_ssripatss_or_block : ssripatss_or_block -> Sexplib0.Sexp.t
Sourceval ssripat_to_yojson : ssripat -> Yojson.Safe.t
Sourceval ssripat_of_yojson : Yojson.Safe.t -> ssripat Ppx_deriving_yojson_runtime.error_or
Sourceval ssripats_to_yojson : ssripats -> Yojson.Safe.t
Sourceval ssripats_of_yojson : Yojson.Safe.t -> ssripats Ppx_deriving_yojson_runtime.error_or
Sourceval ssripatss_to_yojson : ssripatss -> Yojson.Safe.t
Sourceval ssripatss_of_yojson : Yojson.Safe.t -> ssripatss Ppx_deriving_yojson_runtime.error_or
Sourceval ssripatss_or_block_to_yojson : ssripatss_or_block -> Yojson.Safe.t
Sourceval ssripatss_or_block_of_yojson : Yojson.Safe.t -> ssripatss_or_block Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssripat : ssripat Base__Hash.folder
Sourceval hash_fold_ssripats : ssripats Base__Hash.folder
Sourceval hash_fold_ssripatss : Ppx_hash_lib.Std.Hash.state -> ssripatss -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_fold_ssripatss_or_block : Ppx_hash_lib.Std.Hash.state -> ssripatss_or_block -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssripat : ssripat -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_ssripats : ssripats -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_ssripatss : ssripatss -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval hash_ssripatss_or_block : ssripatss_or_block -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssripat : ssripat -> ssripat -> int
Sourceval compare_ssripats : ssripats -> ssripats -> int
Sourceval compare_ssripatss : ssripatss -> ssripatss -> int
Sourceval compare_ssripatss_or_block : ssripatss_or_block -> ssripatss_or_block -> int
Sourcetype ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
Sourceval ssrhpats_of_sexp : Sexplib0.Sexp.t -> ssrhpats
Sourceval sexp_of_ssrhpats : ssrhpats -> Sexplib0.Sexp.t
Sourceval ssrhpats_to_yojson : ssrhpats -> Yojson.Safe.t
Sourceval ssrhpats_of_yojson : Yojson.Safe.t -> ssrhpats Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhpats : Ppx_hash_lib.Std.Hash.state -> ssrhpats -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrhpats : ssrhpats -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrhpats : ssrhpats -> ssrhpats -> int
Sourcetype ssrhpats_wtransp = bool * ssrhpats
Sourceval ssrhpats_wtransp_of_sexp : Sexplib0.Sexp.t -> ssrhpats_wtransp
Sourceval sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Sexplib0.Sexp.t
Sourceval ssrhpats_wtransp_to_yojson : ssrhpats_wtransp -> Yojson.Safe.t
Sourceval ssrhpats_wtransp_of_yojson : Yojson.Safe.t -> ssrhpats_wtransp Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhpats_wtransp : Ppx_hash_lib.Std.Hash.state -> ssrhpats_wtransp -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrhpats_wtransp : ssrhpats_wtransp -> ssrhpats_wtransp -> int
Sourceval ssrintrosarg_of_sexp : Sexplib0.Sexp.t -> ssrintrosarg
Sourceval sexp_of_ssrintrosarg : ssrintrosarg -> Sexplib0.Sexp.t
Sourceval ssrintrosarg_to_yojson : ssrintrosarg -> Yojson.Safe.t
Sourceval ssrintrosarg_of_yojson : Yojson.Safe.t -> ssrintrosarg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrintrosarg : Ppx_hash_lib.Std.Hash.state -> ssrintrosarg -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrintrosarg : ssrintrosarg -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrintrosarg : ssrintrosarg -> ssrintrosarg -> int
Sourcetype ssrfwdid = Names.Id.t
Sourceval ssrfwdid_of_sexp : Sexplib0.Sexp.t -> ssrfwdid
Sourceval sexp_of_ssrfwdid : ssrfwdid -> Sexplib0.Sexp.t
Sourceval ssrfwdid_to_yojson : ssrfwdid -> Yojson.Safe.t
Sourceval ssrfwdid_of_yojson : Yojson.Safe.t -> ssrfwdid Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrfwdid : Ppx_hash_lib.Std.Hash.state -> ssrfwdid -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrfwdid : ssrfwdid -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrfwdid : ssrfwdid -> ssrfwdid -> int
Sourcetype 'term ssrbind = 'term Ssreflect_plugin__Ssrast.ssrbind =
  1. | Bvar of Names.Name.t
  2. | Bdecl of Names.Name.t list * 'term
  3. | Bdef of Names.Name.t * 'term option * 'term
  4. | Bstruct of Names.Name.t
  5. | Bcast of 'term
Sourceval ssrbind_of_sexp : 'term. (Sexplib0.Sexp.t -> 'term) -> Sexplib0.Sexp.t -> 'term ssrbind
Sourceval sexp_of_ssrbind : 'term. ('term -> Sexplib0.Sexp.t) -> 'term ssrbind -> Sexplib0.Sexp.t
Sourceval ssrbind_to_yojson : 'term. ('term -> Yojson.Safe.t) -> 'term ssrbind -> Yojson.Safe.t
Sourceval ssrbind_of_yojson : 'term. (Yojson.Safe.t -> 'term Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'term ssrbind Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrbind : 'term. (Ppx_hash_lib.Std.Hash.state -> 'term -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'term ssrbind -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrbind : 'term. ('term -> 'term -> int) -> 'term ssrbind -> 'term ssrbind -> int
Sourcetype ssrbindfmt = Ssreflect_plugin__Ssrast.ssrbindfmt =
  1. | BFvar
  2. | BFdecl of int
  3. | BFcast
  4. | BFdef
  5. | BFrec of bool * bool
Sourceval ssrbindfmt_of_sexp : Sexplib0.Sexp.t -> ssrbindfmt
Sourceval sexp_of_ssrbindfmt : ssrbindfmt -> Sexplib0.Sexp.t
Sourceval ssrbindfmt_to_yojson : ssrbindfmt -> Yojson.Safe.t
Sourceval ssrbindfmt_of_yojson : Yojson.Safe.t -> ssrbindfmt Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrbindfmt : Ppx_hash_lib.Std.Hash.state -> ssrbindfmt -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrbindfmt : ssrbindfmt -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrbindfmt : ssrbindfmt -> ssrbindfmt -> int
Sourcetype 'term ssrbindval = 'term ssrbind list * 'term
Sourceval ssrbindval_of_sexp : 'term. (Sexplib0.Sexp.t -> 'term) -> Sexplib0.Sexp.t -> 'term ssrbindval
Sourceval sexp_of_ssrbindval : 'term. ('term -> Sexplib0.Sexp.t) -> 'term ssrbindval -> Sexplib0.Sexp.t
Sourceval ssrbindval_to_yojson : 'term. ('term -> Yojson.Safe.t) -> 'term ssrbindval -> Yojson.Safe.t
Sourceval ssrbindval_of_yojson : 'term. (Yojson.Safe.t -> 'term Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'term ssrbindval Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrbindval : 'term. (Ppx_hash_lib.Std.Hash.state -> 'term -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'term ssrbindval -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrbindval : 'term. ('term -> 'term -> int) -> 'term ssrbindval -> 'term ssrbindval -> int
Sourcetype ssrfwdkind = Ssreflect_plugin__Ssrast.ssrfwdkind =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose
Sourceval ssrfwdkind_of_sexp : Sexplib0.Sexp.t -> ssrfwdkind
Sourceval sexp_of_ssrfwdkind : ssrfwdkind -> Sexplib0.Sexp.t
Sourceval ssrfwdkind_to_yojson : ssrfwdkind -> Yojson.Safe.t
Sourceval ssrfwdkind_of_yojson : Yojson.Safe.t -> ssrfwdkind Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrfwdkind : Ppx_hash_lib.Std.Hash.state -> ssrfwdkind -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrfwdkind : ssrfwdkind -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrfwdkind : ssrfwdkind -> ssrfwdkind -> int
Sourcetype ssrfwdfmt = ssrfwdkind * ssrbindfmt list
Sourceval ssrfwdfmt_of_sexp : Sexplib0.Sexp.t -> ssrfwdfmt
Sourceval sexp_of_ssrfwdfmt : ssrfwdfmt -> Sexplib0.Sexp.t
Sourceval ssrfwdfmt_to_yojson : ssrfwdfmt -> Yojson.Safe.t
Sourceval ssrfwdfmt_of_yojson : Yojson.Safe.t -> ssrfwdfmt Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrfwdfmt : Ppx_hash_lib.Std.Hash.state -> ssrfwdfmt -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrfwdfmt : ssrfwdfmt -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrfwdfmt : ssrfwdfmt -> ssrfwdfmt -> int
Sourcetype ssrclseq = Ssreflect_plugin__Ssrast.ssrclseq =
  1. | InGoal
  2. | InHyps
  3. | InHypsGoal
  4. | InHypsSeqGoal
  5. | InSeqGoal
  6. | InHypsSeq
  7. | InAll
  8. | InAllHyps
Sourceval ssrclseq_of_sexp : Sexplib0.Sexp.t -> ssrclseq
Sourceval sexp_of_ssrclseq : ssrclseq -> Sexplib0.Sexp.t
Sourceval ssrclseq_to_yojson : ssrclseq -> Yojson.Safe.t
Sourceval ssrclseq_of_yojson : Yojson.Safe.t -> ssrclseq Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrclseq : Ppx_hash_lib.Std.Hash.state -> ssrclseq -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrclseq : ssrclseq -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrclseq : ssrclseq -> ssrclseq -> int
Sourcetype 'tac ssrhint = bool * 'tac option list
Sourceval ssrhint_of_sexp : 'tac. (Sexplib0.Sexp.t -> 'tac) -> Sexplib0.Sexp.t -> 'tac ssrhint
Sourceval sexp_of_ssrhint : 'tac. ('tac -> Sexplib0.Sexp.t) -> 'tac ssrhint -> Sexplib0.Sexp.t
Sourceval ssrhint_to_yojson : 'tac. ('tac -> Yojson.Safe.t) -> 'tac ssrhint -> Yojson.Safe.t
Sourceval ssrhint_of_yojson : 'tac. (Yojson.Safe.t -> 'tac Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'tac ssrhint Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrhint : 'tac. (Ppx_hash_lib.Std.Hash.state -> 'tac -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'tac ssrhint -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrhint : 'tac. ('tac -> 'tac -> int) -> 'tac ssrhint -> 'tac ssrhint -> int
Sourcetype 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
Sourceval fwdbinders_of_sexp : 'tac. (Sexplib0.Sexp.t -> 'tac) -> Sexplib0.Sexp.t -> 'tac fwdbinders
Sourceval sexp_of_fwdbinders : 'tac. ('tac -> Sexplib0.Sexp.t) -> 'tac fwdbinders -> Sexplib0.Sexp.t
Sourceval fwdbinders_to_yojson : 'tac. ('tac -> Yojson.Safe.t) -> 'tac fwdbinders -> Yojson.Safe.t
Sourceval fwdbinders_of_yojson : 'tac. (Yojson.Safe.t -> 'tac Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'tac fwdbinders Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_fwdbinders : 'tac. (Ppx_hash_lib.Std.Hash.state -> 'tac -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'tac fwdbinders -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_fwdbinders : 'tac. ('tac -> 'tac -> int) -> 'tac fwdbinders -> 'tac fwdbinders -> int
Sourcetype 'tac ffwbinders = ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
Sourceval ffwbinders_of_sexp : 'tac. (Sexplib0.Sexp.t -> 'tac) -> Sexplib0.Sexp.t -> 'tac ffwbinders
Sourceval sexp_of_ffwbinders : 'tac. ('tac -> Sexplib0.Sexp.t) -> 'tac ffwbinders -> Sexplib0.Sexp.t
Sourceval ffwbinders_to_yojson : 'tac. ('tac -> Yojson.Safe.t) -> 'tac ffwbinders -> Yojson.Safe.t
Sourceval ffwbinders_of_yojson : 'tac. (Yojson.Safe.t -> 'tac Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'tac ffwbinders Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ffwbinders : 'tac. (Ppx_hash_lib.Std.Hash.state -> 'tac -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'tac ffwbinders -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ffwbinders : 'tac. ('tac -> 'tac -> int) -> 'tac ffwbinders -> 'tac ffwbinders -> int
Sourcetype clause = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
Sourceval clause_of_sexp : Sexplib0.Sexp.t -> clause
Sourceval sexp_of_clause : clause -> Sexplib0.Sexp.t
Sourceval clause_to_yojson : clause -> Yojson.Safe.t
Sourceval clause_of_yojson : Yojson.Safe.t -> clause Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_clause : Ppx_hash_lib.Std.Hash.state -> clause -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_clause : clause -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_clause : clause -> clause -> int
Sourcetype clauses = clause list * ssrclseq
Sourceval clauses_of_sexp : Sexplib0.Sexp.t -> clauses
Sourceval sexp_of_clauses : clauses -> Sexplib0.Sexp.t
Sourceval clauses_to_yojson : clauses -> Yojson.Safe.t
Sourceval clauses_of_yojson : Yojson.Safe.t -> clauses Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_clauses : Ppx_hash_lib.Std.Hash.state -> clauses -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_clauses : clauses -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_clauses : clauses -> clauses -> int
Sourcetype wgen = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
Sourceval wgen_of_sexp : Sexplib0.Sexp.t -> wgen
Sourceval sexp_of_wgen : wgen -> Sexplib0.Sexp.t
Sourceval wgen_to_yojson : wgen -> Yojson.Safe.t
Sourceval wgen_of_yojson : Yojson.Safe.t -> wgen Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_wgen : Ppx_hash_lib.Std.Hash.state -> wgen -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_wgen : wgen -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_wgen : wgen -> wgen -> int
Sourcetype 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
Sourceval ssrdoarg_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a ssrdoarg
Sourceval sexp_of_ssrdoarg : 'a. ('a -> Sexplib0.Sexp.t) -> 'a ssrdoarg -> Sexplib0.Sexp.t
Sourceval ssrdoarg_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a ssrdoarg -> Yojson.Safe.t
Sourceval ssrdoarg_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssrdoarg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrdoarg : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a ssrdoarg -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrdoarg : 'a. ('a -> 'a -> int) -> 'a ssrdoarg -> 'a ssrdoarg -> int
Sourcetype 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
Sourceval ssrseqarg_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a ssrseqarg
Sourceval sexp_of_ssrseqarg : 'a. ('a -> Sexplib0.Sexp.t) -> 'a ssrseqarg -> Sexplib0.Sexp.t
Sourceval ssrseqarg_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a ssrseqarg -> Yojson.Safe.t
Sourceval ssrseqarg_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssrseqarg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrseqarg : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a ssrseqarg -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrseqarg : 'a. ('a -> 'a -> int) -> 'a ssrseqarg -> 'a ssrseqarg -> int
Sourcetype 'a ssragens = (ssrdocc * 'a) list list * ssrclear
Sourceval ssragens_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a ssragens
Sourceval sexp_of_ssragens : 'a. ('a -> Sexplib0.Sexp.t) -> 'a ssragens -> Sexplib0.Sexp.t
Sourceval ssragens_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a ssragens -> Yojson.Safe.t
Sourceval ssragens_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssragens Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssragens : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a ssragens -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssragens : 'a. ('a -> 'a -> int) -> 'a ssragens -> 'a ssragens -> int
Sourcetype ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
Sourceval ssrapplyarg_of_sexp : Sexplib0.Sexp.t -> ssrapplyarg
Sourceval sexp_of_ssrapplyarg : ssrapplyarg -> Sexplib0.Sexp.t
Sourceval ssrapplyarg_to_yojson : ssrapplyarg -> Yojson.Safe.t
Sourceval ssrapplyarg_of_yojson : Yojson.Safe.t -> ssrapplyarg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrapplyarg : Ppx_hash_lib.Std.Hash.state -> ssrapplyarg -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_ssrapplyarg : ssrapplyarg -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_ssrapplyarg : ssrapplyarg -> ssrapplyarg -> int
Sourcetype 'a ssrcasearg = ssripat option * ('a * ssripats)
Sourceval ssrcasearg_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a ssrcasearg
Sourceval sexp_of_ssrcasearg : 'a. ('a -> Sexplib0.Sexp.t) -> 'a ssrcasearg -> Sexplib0.Sexp.t
Sourceval ssrcasearg_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a ssrcasearg -> Yojson.Safe.t
Sourceval ssrcasearg_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssrcasearg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrcasearg : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a ssrcasearg -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrcasearg : 'a. ('a -> 'a -> int) -> 'a ssrcasearg -> 'a ssrcasearg -> int
Sourcetype 'a ssrmovearg = ssrview * 'a ssrcasearg
Sourceval ssrmovearg_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a ssrmovearg
Sourceval sexp_of_ssrmovearg : 'a. ('a -> Sexplib0.Sexp.t) -> 'a ssrmovearg -> Sexplib0.Sexp.t
Sourceval ssrmovearg_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a ssrmovearg -> Yojson.Safe.t
Sourceval ssrmovearg_of_yojson : 'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssrmovearg Ppx_deriving_yojson_runtime.error_or
Sourceval _ : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a ssrmovearg Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_ssrmovearg : 'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a ssrmovearg -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_ssrmovearg : 'a. ('a -> 'a -> int) -> 'a ssrmovearg -> 'a ssrmovearg -> int
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct