To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
include module type of Ssreflect_plugin.Ssrast
type ssrhyps = ssrhyp list
type ssrsimpl = Ssreflect_plugin.Ssrast.ssrsimpl =
type ssrmult = int * ssrmmod
type ssrindex = int Locus.or_var
type ssrclear = ssrhyps
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
type ast_glob_env = Ssreflect_plugin.Ssrast.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 = Ssreflect_plugin.Ssrast.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 = Ssreflect_plugin.Ssrast.id_block =
| Prefix of Names.Id.t
| SuffixId of Names.Id.t
| SuffixNum of int
type ssripat = Ssreflect_plugin.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 = Ssreflect_plugin.Ssrast.ssripatss_or_block =
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 =
| 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 = Ssreflect_plugin.Ssrast.ssrbindfmt =
type 'term ssrbindval = 'term ssrbind list * 'term
Forward chaining argument
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
type ssrclseq = Ssreflect_plugin.Ssrast.ssrclseq =
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 wgen =
ssrclear
* ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option)
option
type 'a ssrmovearg = ssrview * 'a ssrcasearg
type ssrdgens = Ssreflect_plugin.Ssrast.ssrdgens = {
dgens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
gens : (ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list;
clr : ssrclear;
}
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>