package coq
type uint = | UintVal of Uint31.t| UintDigits of prefix * Names.constructor * lambda array| UintDecomp of prefix * Names.constructor * lambda
and lambda = | Lrel of Names.Name.t * int| Lvar of Names.Id.t| Lmeta of Constr.metavariable * lambda| Levar of Evar.t * lambda * lambda array| Lprod of lambda * lambda| Llam of Names.Name.t array * lambda| Llet of Names.Name.t * lambda * lambda| Lapp of lambda * lambda array| Lconst of prefix * Constr.pconstant| Lproj of prefix * Names.Constant.t| Lprim of prefix * Names.Constant.t * CPrimitives.t * lambda array| Lcase of Nativevalues.annot_sw * lambda * lambda * lam_branches| Lif of lambda * lambda * lambda| Lfix of int array * int * fix_decl| Lcofix of int * fix_decl| Lmakeblock of prefix * Constr.pconstructor * int * lambda array| Lconstruct of prefix * Constr.pconstructor| Luint of uint| Lval of Nativevalues.t| Lsort of Sorts.t| Lind of prefix * Constr.pinductive| Llazy| Lforce
and lam_branches = (Names.constructor * Names.Name.t array * lambda) arrayand fix_decl = Names.Name.t array * lambda array * lambda array