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 =
  1. | AnonHyp of int
  2. | NamedHyp of Names.lident
type explicit_bindings = (quantified_hypothesis * EConstr.t) list
type bindings =
  1. | ImplicitBindings of EConstr.t list
  2. | ExplicitBindings of explicit_bindings
  3. | NoBindings
type constr_with_bindings = EConstr.constr * bindings
type core_destruction_arg =
  1. | ElimOnConstr of constr_with_bindings Proofview.tactic
  2. | ElimOnIdent of Names.Id.t
  3. | ElimOnAnonHyp of int
type destruction_arg = core_destruction_arg
type intro_pattern =
  1. | IntroForthcoming of bool
  2. | IntroNaming of intro_pattern_naming
  3. | IntroAction of intro_pattern_action
and intro_pattern_naming =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous
and intro_pattern_action =
  1. | IntroWildcard
  2. | IntroOrAndPattern of or_and_intro_pattern
  3. | IntroInjection of intro_pattern list
  4. | IntroApplyOn of EConstr.t thunk * intro_pattern
  5. | IntroRewrite of bool
and or_and_intro_pattern =
  1. | IntroOrPattern of intro_pattern list list
  2. | IntroAndPattern of intro_pattern list
type occurrences =
  1. | AllOccurrences
  2. | AllOccurrencesBut of int list
  3. | NoOccurrences
  4. | OnlyOccurrences of int list
type hyp_location_flag = Locus.hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly
type hyp_location = Names.Id.t * occurrences * hyp_location_flag
type clause = {
  1. onhyps : hyp_location list option;
  2. concl_occs : occurrences;
}
type induction_clause = destruction_arg * intro_pattern_naming option * or_and_intro_pattern option * clause option
type multi = Equality.multi =
  1. | Precisely of int
  2. | UpTo of int
  3. | RepeatStar
  4. | RepeatPlus
type orientation = bool
type assertion =
  1. | AssertType of intro_pattern option * EConstr.constr * unit thunk option
  2. | AssertValue of Names.Id.t * EConstr.constr
type format =
  1. | FmtString
  2. | FmtInt
  3. | FmtConstr
  4. | FmtIdent
  5. | FmtLiteral of string
  6. | FmtAlpha
  7. | FmtAlpha0
  8. | FmtMessage
type red_context = (Pattern.constr_pattern * occurrences) option