From 9a3a01fa6e7ef4f53153fc53e8e95aa317ee552c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 May 2019 16:08:52 -0700
Subject: [PATCH] feat(library/compiler/compiler): invoke new IR compiler
 implemented in Lean

---
 src/library/compiler/compiler.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index 5c5c3898fd..9acf1372e6 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -241,10 +241,11 @@ environment compile(environment const & env, options const & opts, names cs) {
     ds = apply(elim_dead_let, ds);
     trace_compiler(name({"compiler", "simp_app_args"}), ds);
     /* compile IR. */
+    new_env = compile_ir(new_env, opts, ds);
+    // TODO: remove rest of the code
     std::tie(new_env, ds) = to_llnf(new_env, ds);
     new_env = save_llnf_code(new_env, ds);
     trace_compiler(name({"compiler", "result"}), ds);
-    // new_env = compile_ir(new_env, opts, ds); // TODO(Leo)
     return new_env;
 }