type evars_flag
= bool
type advanced_flag
= bool
type 'a thunk
= (unit, 'a) Tac2ffi.fun1
type quantified_hypothesis
= Tactypes.quantified_hypothesis
=
type explicit_bindings
= (quantified_hypothesis * EConstr.t) list
type bindings
=
type constr_with_bindings
= EConstr.constr * bindings
type core_destruction_arg
=
type destruction_arg
= core_destruction_arg
type intro_pattern
=
and intro_pattern_naming
=
and intro_pattern_action
=
and or_and_intro_pattern
=
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
=
{
}
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
=