Module Ltac2_plugin.Tac2types

Redefinition of Ltac1 data structures because of impedance mismatch

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.lident
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