package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Serlib_ssr.Ser_ssrastSource

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