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.Old.tactic