diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 0e3cf7b5c9..dd5f6ed021 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -71,7 +71,7 @@ environment mk_projections(environment const & env, name const & n, buffer } expr C_A = mk_app(mk_constant(n, lvls), params); binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info(); - expr c = lctx.mk_local_decl(ngen, name("c"), C_A, c_bi); + expr c = lctx.mk_local_decl(ngen, name("self"), C_A, c_bi); buffer cnstr_type_args; // arguments that are not parameters expr it = cnstr_type; while (is_pi(it)) {