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 * int| Lvar of Names.identifier| Lmeta of Term.metavariable * lambda| Levar of Term.existential * lambda| Lprod of lambda * lambda| Llam of Names.name array * lambda| Llet of Names.name * lambda * lambda| Lapp of lambda * lambda array| Lconst of prefix * Term.pconstant| Lproj of prefix * Names.constant| Lprim of prefix * Names.constant * Primitives.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 * Term.pconstructor * int * lambda array| Lconstruct of prefix * Term.pconstructor| Luint of uint| Lval of Nativevalues.t| Lsort of Term.sorts| Lind of prefix * Term.pinductive| Llazy| Lforce
and lam_branches = (Names.constructor * Names.name array * lambda) arrayand fix_decl = Names.name array * lambda array * lambda array