package coq
type existential_name = Names.Id.ttype cases_pattern_r = | PatVar of Names.Name.t| PatCstr of Names.constructor * cases_pattern list * Names.Name.t
and cases_pattern = cases_pattern_r CAst.ttype 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 * glob_constr) list| GPatVar of Evar_kinds.matching_var_kind| GApp of glob_constr * glob_constr list| GLambda of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr| GProd of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr| GLetIn of Names.Name.t * glob_constr * glob_constr option * glob_constr| GCases of Misctypes.case_style * glob_constr option * tomatch_tuples * cases_clauses| GLetTuple of Names.Name.t list * Names.Name.t * glob_constr option * glob_constr * glob_constr| GIf of glob_constr * Names.Name.t * glob_constr option * glob_constr * glob_constr| GRec of fix_kind * Names.Id.t array * glob_decl list array * glob_constr array * glob_constr array| GSort of Misctypes.glob_sort| GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option| GCast of glob_constr * glob_constr Misctypes.cast_type
and glob_constr = glob_constr_r CAst.tand glob_decl =
Names.Name.t * Decl_kinds.binding_kind * glob_constr option * glob_constrand fix_recursion_order = | GStructRec| GWfRec of glob_constr| GMeasureRec of glob_constr * glob_constr option
and predicate_pattern =
Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located optionand tomatch_tuple = glob_constr * predicate_patternand tomatch_tuples = tomatch_tuple listand cases_clause =
(Names.Id.t list * cases_pattern list * glob_constr) Loc.locatedand cases_clauses = cases_clause listtype extended_glob_local_binder_r = | GLocalAssum of Names.Name.t * Decl_kinds.binding_kind * glob_constr| GLocalDef of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr option| GLocalPattern of cases_pattern * Names.Id.t list * Names.Id.t * Decl_kinds.binding_kind * glob_constr
and extended_glob_local_binder = extended_glob_local_binder_r CAst.ttype closure = {idents : Names.Id.t Names.Id.Map.t;typed : Pattern.constr_under_binders Names.Id.Map.t;untyped : closed_glob_constr Names.Id.Map.t;
}type var_map = Pattern.constr_under_binders Names.Id.Map.ttype uconstr_var_map = closed_glob_constr Names.Id.Map.ttype unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.ttype ltac_var_map = {ltac_constrs : var_map;ltac_uconstrs : uconstr_var_map;ltac_idents : Names.Id.t Names.Id.Map.t;ltac_genargs : unbound_ltac_var_map;
}