From df9c935f0a8b1879918f275f39b4334bc6bdbd30 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 May 2014 17:02:20 -0700 Subject: [PATCH] fix(kernel/inductive): remove unused argument, bug in is_rec_argument (free variable occurrence) Signed-off-by: Leonardo de Moura --- src/kernel/inductive/inductive.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 1c821a68e..c240f1857 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -318,7 +318,7 @@ struct add_inductive_fn { optional is_rec_argument(expr t) { t = m_tc.whnf(t); while (is_pi(t)) - t = m_tc.whnf(binding_body(t)); + t = m_tc.whnf(instantiate(binding_body(t), mk_local_for(t))); return is_valid_it_app(t); } @@ -345,7 +345,7 @@ struct add_inductive_fn { \see check_intro_rules */ - void check_intro_rule(inductive_decl const &, unsigned d_idx, intro_rule const & ir) { + void check_intro_rule(unsigned d_idx, intro_rule const & ir) { expr t = intro_rule_type(ir); name n = intro_rule_name(ir); m_tc.check(t, m_level_names); @@ -400,7 +400,7 @@ struct add_inductive_fn { unsigned i = 0; for (auto d : m_decls) { for (auto ir : inductive_decl_intros(d)) - check_intro_rule(d, i, ir); + check_intro_rule(i, ir); i++; } }