Module Ssreflect_plugin.Ssrast

type ssrhyp =
| SsrHyp of Names.Id.t Loc.located
type ssrhyp_or_id =
| Hyp of ssrhyp
| Id of ssrhyp
type ssrhyps = ssrhyp list
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir =
| L2R
| R2L
type ssrsimpl =
| Simpl of int
| Cut of int
| SimplCut of int * int
| Nop
type ssrmmod =
| May
| Must
| Once
type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option

Occurrence switch

2

, all is Some(false,)

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 = {
ast_ltacvars : Names.Id.Set.t;
ast_extra : Genintern.Store.t;
ast_intern_sign : Genintern.intern_variable_status;
}
type ast_closure_term = {
body : Constrexpr.constr_expr;
glob_env : ast_glob_env option;
interp_env : Geninterp.interp_sign option;
annotation : [ `None | `Parens | `DoubleParens | `At ];
}
type ssrview = ast_closure_term list
type id_block =
| Prefix of Names.Id.t
| SuffixId of Names.Id.t
| SuffixNum of int
type anon_kind =
| One of string option
| Drop
| All
| Temporary
type 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 =
| 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 =
| 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

Binders (for fwd tactics)

type ssrbindfmt =
| BFvar
| BFdecl of int
| BFcast
| BFdef
| BFrec of bool * bool
type 'term ssrbindval = 'term ssrbind list * 'term
type ssrfwdkind =
| FwdHint of string * bool
| FwdHave
| FwdPose

Forward chaining argument

type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
type 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 = {
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