package coq-serapi

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