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
module Proofview : sig ... end
type ssrhyp = Ssrast.ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
val ssrhyp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp
val sexp_of_ssrhyp : ssrhyp -> Ppx_sexp_conv_lib.Sexp.t
type ssrhyp_or_id = Ssrast.ssrhyp_or_id =
  1. | Hyp of ssrhyp
  2. | Id of ssrhyp
val ssrhyp_or_id_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyp_or_id
val sexp_of_ssrhyp_or_id : ssrhyp_or_id -> Ppx_sexp_conv_lib.Sexp.t
type ssrhyps = ssrhyp list
val ssrhyps_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhyps
val sexp_of_ssrhyps : ssrhyps -> Ppx_sexp_conv_lib.Sexp.t
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
  1. | L2R
  2. | R2L
val ssrdir_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdir
val sexp_of_ssrdir : ssrdir -> Ppx_sexp_conv_lib.Sexp.t
type ssrsimpl = Ssrast.ssrsimpl =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
val ssrsimpl_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrsimpl
val sexp_of_ssrsimpl : ssrsimpl -> Ppx_sexp_conv_lib.Sexp.t
type ssrmmod = Ssrast.ssrmmod =
  1. | May
  2. | Must
  3. | Once
val ssrmmod_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmmod
val sexp_of_ssrmmod : ssrmmod -> Ppx_sexp_conv_lib.Sexp.t
type ssrmult = int * ssrmmod
val ssrmult_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrmult
val sexp_of_ssrmult : ssrmult -> Ppx_sexp_conv_lib.Sexp.t
type ssrocc = (bool * int list) option
val ssrocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrocc
val sexp_of_ssrocc : ssrocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrindex = int Locus.or_var
val ssrindex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrindex
val sexp_of_ssrindex : ssrindex -> Ppx_sexp_conv_lib.Sexp.t
type ssrclear = ssrhyps
val ssrclear_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclear
val sexp_of_ssrclear : ssrclear -> Ppx_sexp_conv_lib.Sexp.t
type ssrdocc = ssrclear option * ssrocc
val ssrdocc_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrdocc
val sexp_of_ssrdocc : ssrdocc -> Ppx_sexp_conv_lib.Sexp.t
type ssrtermkind = char
val ssrtermkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrtermkind
val sexp_of_ssrtermkind : ssrtermkind -> Ppx_sexp_conv_lib.Sexp.t
val ssrterm_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrterm
val sexp_of_ssrterm : ssrterm -> Ppx_sexp_conv_lib.Sexp.t
type ast_glob_env = 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 : Ppx_sexp_conv_lib.Sexp.t -> ast_glob_env
val sexp_of_ast_glob_env : ast_glob_env -> Ppx_sexp_conv_lib.Sexp.t
type ast_closure_term = 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 : Ppx_sexp_conv_lib.Sexp.t -> ast_closure_term
val sexp_of_ast_closure_term : ast_closure_term -> Ppx_sexp_conv_lib.Sexp.t
type ssrview = ast_closure_term list
val ssrview_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrview
val sexp_of_ssrview : ssrview -> Ppx_sexp_conv_lib.Sexp.t
type anon_kind = Ssrast.anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
val anon_kind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> anon_kind
val sexp_of_anon_kind : anon_kind -> Ppx_sexp_conv_lib.Sexp.t
type id_block = Ssrast.id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
val id_block_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> id_block
val sexp_of_id_block : id_block -> Ppx_sexp_conv_lib.Sexp.t
type ssripat = 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 = 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 : Ppx_sexp_conv_lib.Sexp.t -> ssripatss
val ssripatss_or_block_of_sexp : Ppx_sexp_conv_lib.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 -> Ppx_sexp_conv_lib.Sexp.t
val sexp_of_ssripatss_or_block : ssripatss_or_block -> Ppx_sexp_conv_lib.Sexp.t
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
val ssrhpats_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats
val sexp_of_ssrhpats : ssrhpats -> Ppx_sexp_conv_lib.Sexp.t
type ssrhpats_wtransp = bool * ssrhpats
val ssrhpats_wtransp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrhpats_wtransp
val sexp_of_ssrhpats_wtransp : ssrhpats_wtransp -> Ppx_sexp_conv_lib.Sexp.t
val ssrintrosarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrintrosarg
val sexp_of_ssrintrosarg : ssrintrosarg -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdid = Names.Id.t
val ssrfwdid_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdid
val sexp_of_ssrfwdid : ssrfwdid -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbind = 'term 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. (Ppx_sexp_conv_lib.Sexp.t -> 'term) -> Ppx_sexp_conv_lib.Sexp.t -> 'term ssrbind
val sexp_of_ssrbind : 'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) -> 'term ssrbind -> Ppx_sexp_conv_lib.Sexp.t
type ssrbindfmt = Ssrast.ssrbindfmt =
  1. | BFvar
  2. | BFdecl of int
  3. | BFcast
  4. | BFdef
  5. | BFrec of bool * bool
val ssrbindfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrbindfmt
val sexp_of_ssrbindfmt : ssrbindfmt -> Ppx_sexp_conv_lib.Sexp.t
type 'term ssrbindval = 'term ssrbind list * 'term
val ssrbindval_of_sexp : 'term. (Ppx_sexp_conv_lib.Sexp.t -> 'term) -> Ppx_sexp_conv_lib.Sexp.t -> 'term ssrbindval
val sexp_of_ssrbindval : 'term. ('term -> Ppx_sexp_conv_lib.Sexp.t) -> 'term ssrbindval -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdkind = Ssrast.ssrfwdkind =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose
val ssrfwdkind_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdkind
val sexp_of_ssrfwdkind : ssrfwdkind -> Ppx_sexp_conv_lib.Sexp.t
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
val ssrfwdfmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrfwdfmt
val sexp_of_ssrfwdfmt : ssrfwdfmt -> Ppx_sexp_conv_lib.Sexp.t
type ssrclseq = Ssrast.ssrclseq =
  1. | InGoal
  2. | InHyps
  3. | InHypsGoal
  4. | InHypsSeqGoal
  5. | InSeqGoal
  6. | InHypsSeq
  7. | InAll
  8. | InAllHyps
val ssrclseq_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrclseq
val sexp_of_ssrclseq : ssrclseq -> Ppx_sexp_conv_lib.Sexp.t
type 'tac ssrhint = bool * 'tac option list
val ssrhint_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac ssrhint
val sexp_of_ssrhint : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac ssrhint -> Ppx_sexp_conv_lib.Sexp.t
type 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
val fwdbinders_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac fwdbinders
val sexp_of_fwdbinders : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac fwdbinders -> Ppx_sexp_conv_lib.Sexp.t
type 'tac ffwbinders = ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
val ffwbinders_of_sexp : 'tac. (Ppx_sexp_conv_lib.Sexp.t -> 'tac) -> Ppx_sexp_conv_lib.Sexp.t -> 'tac ffwbinders
val sexp_of_ffwbinders : 'tac. ('tac -> Ppx_sexp_conv_lib.Sexp.t) -> 'tac ffwbinders -> Ppx_sexp_conv_lib.Sexp.t
type clause = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
val clause_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clause
val sexp_of_clause : clause -> Ppx_sexp_conv_lib.Sexp.t
type clauses = clause list * ssrclseq
val clauses_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> clauses
val sexp_of_clauses : clauses -> Ppx_sexp_conv_lib.Sexp.t
type wgen = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
val wgen_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> wgen
val sexp_of_wgen : wgen -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
val ssrdoarg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrdoarg
val sexp_of_ssrdoarg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrdoarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
val ssrseqarg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrseqarg
val sexp_of_ssrseqarg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrseqarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssragens = (ssrdocc * 'a) list list * ssrclear
val ssragens_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssragens
val sexp_of_ssragens : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssragens -> Ppx_sexp_conv_lib.Sexp.t
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
val ssrapplyarg_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> ssrapplyarg
val sexp_of_ssrapplyarg : ssrapplyarg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrcasearg = ssripat option * ('a * ssripats)
val ssrcasearg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrcasearg
val sexp_of_ssrcasearg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrcasearg -> Ppx_sexp_conv_lib.Sexp.t
type 'a ssrmovearg = ssrview * 'a ssrcasearg
val ssrmovearg_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a ssrmovearg
val sexp_of_ssrmovearg : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a ssrmovearg -> Ppx_sexp_conv_lib.Sexp.t
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