From 7bf3e2ffbb8545cf8cff4d938f73c4280ebf9705 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 May 2016 16:47:53 -0700 Subject: [PATCH] fix(compiler/simp_pr1_rec): typo --- src/compiler/simp_pr1_rec.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/compiler/simp_pr1_rec.cpp b/src/compiler/simp_pr1_rec.cpp index e17c4f007c..7d367e8616 100644 --- a/src/compiler/simp_pr1_rec.cpp +++ b/src/compiler/simp_pr1_rec.cpp @@ -117,7 +117,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor { // Step 1. for (unsigned k = 0; k < minor_ctx.size(); k++) { if (minor_is_rec_arg[k]) { - expr type = ctx().whnf(minor_ctx[k]); + expr type = ctx().whnf(ctx().infer(minor_ctx[k])); buffer type_args; expr type_fn = get_app_args(type, type_args); if (!is_constant(type_fn) || const_name(type_fn) != get_prod_name() || type_args.size() != 2)