package coq
type patvar = Names.Id.ttype !'constr intro_pattern_expr = | IntroForthcoming of bool| IntroNaming of intro_pattern_naming_expr| IntroAction of 'constr intro_pattern_action_expr
and intro_pattern_naming_expr = | IntroIdentifier of Names.Id.t| IntroFresh of Names.Id.t| IntroAnonymous
and !'constr intro_pattern_action_expr = | IntroWildcard| IntroOrAndPattern of 'constr or_and_intro_pattern_expr| IntroInjection of 'constr intro_pattern_expr Loc.located list| IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located| IntroRewrite of bool
and !'constr or_and_intro_pattern_expr = | IntroOrPattern of 'constr intro_pattern_expr Loc.located list list| IntroAndPattern of 'constr intro_pattern_expr Loc.located list
type sort_info = Names.Name.t Loc.located listtype level_info = Names.Name.t Loc.located optiontype glob_sort = sort_info glob_sort_gentype glob_level = level_info glob_sort_gentype existential_key = Evar.ttype !'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located listtype !'a bindings = | ImplicitBindings of 'a list| ExplicitBindings of 'a explicit_bindings| NoBindings
type !'a with_bindings = 'a * 'a bindingstype !'a and_short_name = 'a * Names.Id.t Loc.located optiontype !'a core_destruction_arg = | ElimOnConstr of 'a| ElimOnIdent of Names.Id.t Loc.located| ElimOnAnonHyp of int
type !'a destruction_arg = clear_flag * 'a core_destruction_arg