From 06b02e4912005359393ab81987606f51fa329f3c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Aug 2016 21:00:57 -0700 Subject: [PATCH] chore(library/equations_compiler): test elim_match on nonrec equations --- src/library/equations_compiler/compiler.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index 4b0bf79eaf..86db3840d4 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -29,6 +29,8 @@ expr compile_equations(environment & env, options const & opts, metavar_context optional eqns1 = try_structural_rec(ctx.get(), eqns, arg_idx); if (eqns1) { elim_match(env, opts, mctx, lctx, *eqns1); + } else if (!is_recursive_eqns(ctx, eqns)) { + elim_match(env, opts, mctx, lctx, eqns); } // test unbounded_rec