From cf49e6fe8f0976766dc6d518c8c01727863049e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Aug 2021 11:11:37 -0700 Subject: [PATCH] fix: binder name Binder names are relevant for the `induction` tactic. --- src/kernel/quot.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp index 84c0b7676f..a76bc05628 100644 --- a/src/kernel/quot.cpp +++ b/src/kernel/quot.cpp @@ -92,7 +92,7 @@ environment environment::add_quot() const { /* constant {u} quot.ind {α : Sort u} {r : α → α → Prop} {β : @quot.{u} α r → Prop} : (∀ a : α, β (@quot.mk.{u} α r a)) → ∀ q : @quot.{u} α r, β q */ new_env.add_core(constant_info(quot_val(*quot_consts::g_quot_ind, {u_name}, - lctx.mk_pi({alpha, r, beta}, mk_arrow(all_quot, lctx.mk_pi(q, beta_q))), quot_kind::Ind))); + lctx.mk_pi({alpha, r, beta}, mk_pi("mk", all_quot, lctx.mk_pi(q, beta_q))), quot_kind::Ind))); new_env.mark_quot_initialized(); return new_env; }