package coq
type existential_name = Names.Id.ttype !'a cases_pattern_r = | PatVar of Names.Name.t| PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t
and !'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.ttype cases_pattern = [ `any ] cases_pattern_gtype !'a glob_constr_r = | GRef of Globnames.global_reference * Misctypes.glob_level list option| GVar of Names.Id.t| GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list| GPatVar of Evar_kinds.matching_var_kind| GApp of 'a glob_constr_g * 'a glob_constr_g list| GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g| GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g| GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g| GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g| GLetTuple of Names.Name.t list * Names.Name.t * 'a glob_constr_g option * 'a glob_constr_g * 'a glob_constr_g| GIf of 'a glob_constr_g * Names.Name.t * 'a glob_constr_g option * 'a glob_constr_g * 'a glob_constr_g| GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array| GSort of Misctypes.glob_sort| GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option| GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type
and !'a glob_constr_g = ('a glob_constr_r, 'a) DAst.tand !'a glob_decl_g =
Names.Name.t
* Decl_kinds.binding_kind
* 'a glob_constr_g option
* 'a glob_constr_gand !'a fix_recursion_order_g = | GStructRec| GWfRec of 'a glob_constr_g| GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
and 'a predicate_pattern_g =
Names.Name.t * (Names.inductive * Names.Name.t list) CAst.t optionand !'a tomatch_tuple_g = 'a glob_constr_g * 'a predicate_pattern_gand !'a tomatch_tuples_g = 'a tomatch_tuple_g listand !'a cases_clause_g =
(Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.tand !'a cases_clauses_g = 'a cases_clause_g listtype glob_constr = [ `any ] glob_constr_gtype tomatch_tuple = [ `any ] tomatch_tuple_gtype tomatch_tuples = [ `any ] tomatch_tuples_gtype cases_clause = [ `any ] cases_clause_gtype cases_clauses = [ `any ] cases_clauses_gtype glob_decl = [ `any ] glob_decl_gtype fix_kind = [ `any ] fix_kind_gtype predicate_pattern = [ `any ] predicate_pattern_gtype fix_recursion_order = [ `any ] fix_recursion_order_gtype !'a disjunctive_cases_clause_g =
(Names.Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.ttype !'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g listtype !'a cases_pattern_disjunction_g = 'a cases_pattern_g listtype disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_gtype disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_gtype cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_gtype !'a extended_glob_local_binder_r = | GLocalAssum of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g| GLocalDef of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g option| GLocalPattern of 'a cases_pattern_disjunction_g * Names.Id.t list * Names.Id.t * Decl_kinds.binding_kind * 'a glob_constr_g
and !'a extended_glob_local_binder_g =
('a extended_glob_local_binder_r, 'a) DAst.ttype extended_glob_local_binder = [ `any ] extended_glob_local_binder_g