Combinatorstelescope env sigma ctx turns a context x1:A1;...;xn:An into a right-associated nested sigma-type of the right sort. It returns:
T := {x1:A1 & ... {xn-1:An-1 & ... An} ... }(existsT _ x1 ... (existsT _ xn-1 xn) ...) inhabiting the sigma-type in the given contextctx with values they have in the context x:T, that is x1:=projT1 x;...;xn-1:=projT1 ... (projT2 x);xn:=projT2 ... (projT2 x); note that let-ins in the original context are preserved Depending on the sorts of types, it uses either ex, sig or sigT, even if we always used sigT above as an example.val telescope : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Evd.evar_map * EConstr.rel_context * telescopemake_iterated_tuple env sigma ~default c encapsulates c (of inferred type C) and its free variables x1,...,xn into a right-associated nested tuple in a sigT-type. It returns:
{x1:A1 & ... {xn:An & ... C} ... }(existsT _ x1 ... (existsT _ xn c) ...)(existsT _ x1 ... (existsT _ xn default) ...); if default has not the right type, it fails.val make_iterated_tuple : Environ.env -> Evd.evar_map -> default:EConstr.constr -> EConstr.constr -> EConstr.types -> Evd.evar_map * telescope * EConstr.constrmake_selector env sigma ~pos ~special ~default c constructs a case-split on c (assumed of inductive type), with the pos-th branch returning special, and all the other branch returning default.
val make_selector : Environ.env -> Evd.evar_map -> pos:int -> special:EConstr.constr -> default:EConstr.constr -> EConstr.constr -> EConstr.types -> EConstr.constr