Module Combinators

telescope env sigma ctx turns a context x1:A1;...;xn:An into a right-associated nested sigma-type of the right sort. It returns:

type telescope = {
telescope_type : EConstr.types;
telescope_value : EConstr.constr;

make_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:

make_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