package coq
type lident = Names.Id.t CAst.ttype lname = Names.Name.t CAst.ttype lstring = string CAst.ttype 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 CAst.t list| IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t| IntroRewrite of bool
and !'constr or_and_intro_pattern_expr = | IntroOrPattern of 'constr intro_pattern_expr CAst.t list list| IntroAndPattern of 'constr intro_pattern_expr CAst.t list
type level_info = Libnames.reference universe_kindtype glob_level = level_info glob_sort_gentype glob_constraint = glob_level * Univ.constraint_type * glob_leveltype sort_info = (Libnames.reference * int) option listtype glob_sort = sort_info glob_sort_gentype existential_key = Evar.ttype case_style = Constr.case_style = type !'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t 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 * lident optiontype !'a or_by_notation = 'a or_by_notation_r CAst.ttype !'a destruction_arg = clear_flag * 'a core_destruction_arg