package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

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

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.20.0.0.20.0.tbz
sha256=ead9382f111ea385008fe9037513ff1f738dd90d8e989b8d1a0c9290963d9afe
sha512=b29103c2d1eb3cf8a33fa9ddf26b5a6c89e7277cd31256589bcae8a89c37a3de7a3c3e7fe5d376358e874d44dc6c60ab96736cbd1037511ab36705e9f40f0ade

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