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.16.0.0.16.2.tbz
sha256=f891507f58fba3ba29889dd07fbe69af3411d246488ae7595cd81d26c8422f14
sha512=224dfda8fae1ead7a5ae2a8ead527834bb5216b1788485a0c19deade3b0dd86767c19056931294a7973f132680e282c4491c76ef38638c0c566a029379f484e2

doc/serlib_ssr/Serlib_ssr/Wrap_ssrast/index.html

Module Serlib_ssr.Wrap_ssrastSource

Sourcemodule Ssreflect_plugin : sig ... end
Sourcemodule Wrap : sig ... end
include module type of struct include Wrap end
include module type of Ssreflect_plugin.Ssrast
type ssrhyp = Ssreflect_plugin__Ssrast.ssrhyp =
  1. | SsrHyp of Names.Id.t Loc.located
type ssrhyp_or_id = Ssreflect_plugin__Ssrast.ssrhyp_or_id =
  1. | Hyp of ssrhyp
  2. | Id of ssrhyp
type ssrhyps = ssrhyp list
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
  1. | L2R
  2. | R2L
type ssrsimpl = Ssreflect_plugin__Ssrast.ssrsimpl =
  1. | Simpl of int
  2. | Cut of int
  3. | SimplCut of int * int
  4. | Nop
type ssrmmod = Ssreflect_plugin__Ssrast.ssrmmod =
  1. | May
  2. | Must
  3. | Once
type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
type ssrindex = int Locus.or_var
type ssrclear = ssrhyps
type ssrdocc = ssrclear option * ssrocc
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
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;
}
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 | `None | `Parens ];
}
type ssrview = ast_closure_term list
type id_block = Ssreflect_plugin__Ssrast.id_block =
  1. | Prefix of Names.Id.t
  2. | SuffixId of Names.Id.t
  3. | SuffixNum of int
type anon_kind = Ssreflect_plugin__Ssrast.anon_kind =
  1. | One of string option
  2. | Drop
  3. | All
  4. | Temporary
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
type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
type ssrhpats_wtransp = bool * ssrhpats
type ssrintrosarg = Ltac_plugin.Tacexpr.raw_tactic_expr * ssripats
type ssrfwdid = Names.Id.t
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
type ssrbindfmt = Ssreflect_plugin__Ssrast.ssrbindfmt =
  1. | BFvar
  2. | BFdecl of int
  3. | BFcast
  4. | BFdef
  5. | BFrec of bool * bool
type !'term ssrbindval = 'term ssrbind list * 'term
type ssrfwdkind = Ssreflect_plugin__Ssrast.ssrfwdkind =
  1. | FwdHint of string * bool
  2. | FwdHave
  3. | FwdPose
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
type ssrclseq = Ssreflect_plugin__Ssrast.ssrclseq =
  1. | InGoal
  2. | InHyps
  3. | InHypsGoal
  4. | InHypsSeqGoal
  5. | InSeqGoal
  6. | InHypsSeq
  7. | InAll
  8. | InAllHyps
type !'tac ssrhint = bool * 'tac option list
type !'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
type !'tac ffwbinders = ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)
type clause = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
type clauses = clause list * ssrclseq
type wgen = ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option
type !'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
type !'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
type !'a ssrcasearg = ssripat option * ('a * ssripats)
type !'a ssrmovearg = ssrview * 'a ssrcasearg
type ssrdgens = Ssreflect_plugin__Ssrast.ssrdgens = {
  1. dgens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
  2. gens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
  3. clr : ssrclear;
}
type !'a ssragens = (ssrdocc * 'a) list list * ssrclear
type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats)
type gist = Ltac_plugin.Tacintern.glob_sign
type ist = Ltac_plugin.Tacinterp.interp_sign
type goal = Evar.t