From b3d78208be21f207251f6e4abe1cbe057604e791 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Sep 2016 12:39:21 -0700 Subject: [PATCH] fix(library/equations_compiler/elim_match): typo --- src/library/equations_compiler/elim_match.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index f58292e74b..665968a510 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -644,7 +644,7 @@ struct elim_match_fn { expr new_arg = ctx.push_local(binding_name(it), binding_domain(it)); new_args.push_back(new_arg); c = mk_app(c, new_arg); - it = whnf_inductive(ctx, instantiate(binding_body(new_arg), new_arg)); + it = whnf_inductive(ctx, instantiate(binding_body(it), new_arg)); } if (ctx.is_def_eq(pattern_type, it)) { equation new_eqn = eqn;