Module `Ltac2_plugin.Tac2types`

type evars_flag = bool
type advanced_flag = bool
type 'a thunk = (unit, 'a) Tac2ffi.fun1
type quantified_hypothesis = Tactypes.quantified_hypothesis = | AnonHyp of int | NamedHyp of Names.Id.t
type explicit_bindings = (quantified_hypothesis * EConstr.t) list
type bindings = | ImplicitBindings of EConstr.t list | ExplicitBindings of explicit_bindings | NoBindings
type constr_with_bindings = EConstr.constr * bindings
type core_destruction_arg = | ElimOnConstr of constr_with_bindings Proofview.tactic | ElimOnIdent of Names.Id.t | ElimOnAnonHyp of int
type destruction_arg = core_destruction_arg
type intro_pattern = | IntroForthcoming of bool | IntroNaming of intro_pattern_naming | IntroAction of intro_pattern_action
and intro_pattern_naming = | IntroIdentifier of Names.Id.t | IntroFresh of Names.Id.t | IntroAnonymous
and intro_pattern_action = | IntroWildcard | IntroOrAndPattern of or_and_intro_pattern | IntroInjection of intro_pattern list | IntroApplyOn of EConstr.t thunk * intro_pattern | IntroRewrite of bool
and or_and_intro_pattern = | IntroOrPattern of intro_pattern list list | IntroAndPattern of intro_pattern list
type occurrences = | AllOccurrences | AllOccurrencesBut of int list | NoOccurrences | OnlyOccurrences of int list
type hyp_location_flag = Locus.hyp_location_flag = | InHyp | InHypTypeOnly | InHypValueOnly
type hyp_location = Names.Id.t * occurrences * hyp_location_flag
type clause = { onhyps : hyp_location list option; concl_occs : occurrences; }
type induction_clause = destruction_arg * intro_pattern_naming option * or_and_intro_pattern option * clause option
type multi = Equality.multi = | Precisely of int | UpTo of int | RepeatStar | RepeatPlus
type rewriting = bool option * multi * constr_with_bindings Proofview.tactic
type assertion = | AssertType of intro_pattern option * EConstr.constr * unit thunk option | AssertValue of Names.Id.t * EConstr.constr