package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

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

Authors

Maintainers

E

e@x80.org

Sources

coq-serapi-8.10.0.0.7.0.tbz

sha256=4448c2b45a6975d7a90d3e07ce75386103d3e17c8ad96c566da854ac1e56802c

sha512=19027ca59703c8b74abd372e14403d22d07e9e8c248a50ae8f880647c10ee1f22cee93587583374c96971a667e10546b4997ff7b6a91aea51b51bbacb3052ee4

doc/serlib_ssr/Wrap_ssrast/index.html

Module `Wrap_ssrast`

module Ssreflect_plugin : sig ... end

module Wrap : sig ... end

include module type of struct include Wrap end

include module type of Ssreflect_plugin.Ssrast

type ssrhyp = Ssrast.ssrhyp =

| SsrHyp of Names.Id.t Loc.located

type ssrhyp_or_id = Ssrast.ssrhyp_or_id =

| Hyp of ssrhyp
| Id of ssrhyp

type ssrhyps = ssrhyp list

type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =

| L2R
| R2L

type ssrsimpl = Ssrast.ssrsimpl =

| Simpl of int
| Cut of int
| SimplCut of int * int
| Nop

type ssrmmod = Ssrast.ssrmmod =

| May
| Must
| 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 = char

type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr

type ast_closure_term = Ssrast.ast_closure_term = {

body : Constrexpr.constr_expr;
glob_env : Genintern.glob_sign option;
interp_env : Geninterp.interp_sign option;
annotation : [ `At | `DoubleParens | `None | `Parens ];

}

type ssrview = ast_closure_term list

type id_block = Ssrast.id_block =

| Prefix of Names.Id.t
| SuffixId of Names.Id.t
| SuffixNum of int

type anon_kind = Ssrast.anon_kind =

| One of string option
| Drop
| All
| Temporary

type ssripat = Ssrast.ssripat =

| IPatNoop
| IPatId of Names.Id.t
| IPatAnon of anon_kind
| IPatDispatch of ssripatss_or_block
| IPatCase of ssripatss_or_block
| IPatInj of ssripatss
| IPatRewrite of ssrocc * ssrdir
| IPatView of ssrview
| IPatClear of ssrclear
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Names.Id.t list
| IPatFastNondep

and ssripats = ssripat list

and ssripatss = ssripats list

and ssripatss_or_block = Ssrast.ssripatss_or_block =

| Block of id_block
| 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 Ssrast.ssrbind =

| Bvar of Names.Name.t
| Bdecl of Names.Name.t list * 'term
| Bdef of Names.Name.t * 'term option * 'term
| Bstruct of Names.Name.t
| Bcast of 'term

type ssrbindfmt = Ssrast.ssrbindfmt =

| BFvar
| BFdecl of int
| BFcast
| BFdef
| BFrec of bool * bool

type !'term ssrbindval = 'term ssrbind list * 'term

type ssrfwdkind = Ssrast.ssrfwdkind =

| FwdHint of string * bool
| FwdHave
| FwdPose

type ssrfwdfmt = ssrfwdkind * ssrbindfmt list

type ssrclseq = Ssrast.ssrclseq =

| InGoal
| InHyps
| InHypsGoal
| InHypsSeqGoal
| InSeqGoal
| InHypsSeq
| InAll
| 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 = Ssrast.ssrdgens = {

dgens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
gens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
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 = Goal.goal

type !'a sigma = 'a Evd.sigma

type v82tac = Tacmach.tactic