diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 871d0fe6f..5ed76cb7c 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -426,12 +426,8 @@ class frontend_elaborator::imp {
         }
     };
 
-    metavar_env elaborate_core() {
-        // std::stable_sort(m_ucs.begin(), m_ucs.end(),
-        //                 [](unification_constraint const & c1, unification_constraint const & c2) {
-        //                     return !is_choice(c1) && is_choice(c2);
-        //                 });
-        elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data());
+    metavar_env elaborate_core(options const & opts) {
+        elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data(), opts);
         return elb.next();
     }
 
@@ -442,7 +438,7 @@ public:
         m_normalizer(m_env) {
     }
 
-    std::pair<expr, metavar_env> elaborate(expr const & e) {
+    std::pair<expr, metavar_env> elaborate(expr const & e, options const & opts) {
         // std::cout << "Elaborate " << e << "\n";
         clear();
         expr new_e = preprocessor(*this)(e);
@@ -453,14 +449,15 @@ public:
             //     formatter fmt = mk_simple_formatter();
             //     std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
-            metavar_env new_menv = elaborate_core();
+            metavar_env new_menv = elaborate_core(opts);
             return mk_pair(new_menv->instantiate_metavars(new_e), new_menv);
         } else {
             return mk_pair(new_e, metavar_env());
         }
     }
 
-    std::tuple<expr, expr, metavar_env> elaborate(name const & n, expr const & t, expr const & e) {
+    std::tuple<expr, expr, metavar_env> elaborate(name const & n, expr const & t, expr const & e,
+                                                  options const & opts) {
         // std::cout << "Elaborate " << t << " : " << e << "\n";
         clear();
         expr new_t = preprocessor(*this)(t);
@@ -475,7 +472,7 @@ public:
             //    formatter fmt = mk_simple_formatter();
             //    std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
             // }
-            metavar_env new_menv = elaborate_core();
+            metavar_env new_menv = elaborate_core(opts);
             return std::make_tuple(new_menv->instantiate_metavars(new_t),
                                    new_menv->instantiate_metavars(new_e),
                                    new_menv);
@@ -511,9 +508,12 @@ public:
 
 frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(std::make_shared<imp>(env)) {}
 frontend_elaborator::~frontend_elaborator() {}
-std::pair<expr, metavar_env> frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
-std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) {
-    return m_ptr->elaborate(n, t, e);
+std::pair<expr, metavar_env> frontend_elaborator::operator()(expr const & e, options const & opts) {
+    return m_ptr->elaborate(e, opts);
+}
+std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e,
+                                                                    options const & opts) {
+    return m_ptr->elaborate(n, t, e, opts);
 }
 expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
 void frontend_elaborator::clear() { m_ptr->clear(); }
diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h
index e04107e53..f6219e478 100644
--- a/src/frontends/lean/frontend_elaborator.h
+++ b/src/frontends/lean/frontend_elaborator.h
@@ -29,13 +29,13 @@ public:
     /**
        \brief Elaborate the given expression.
     */
-    std::pair<expr, metavar_env> operator()(expr const & e);
+    std::pair<expr, metavar_env> operator()(expr const & e, options const & opts);
     /**
        \brief Elaborate the given type and expression. The typeof(e) == t.
        This information is used by the elaborator. The result is a new
        elaborated type and expression.
     */
-    std::tuple<expr, expr, metavar_env> operator()(name const & n, expr const & t, expr const & e);
+    std::tuple<expr, expr, metavar_env> operator()(name const & n, expr const & t, expr const & e, options const & opts);
 
     /**
         \brief If \c e is an expression instantiated by the elaborator, then it
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 81e392eac..3d473cacf 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -148,7 +148,7 @@ void parser_imp::parse_def_core(bool is_definition) {
             pre_val   = mk_abstraction(expr_kind::Lambda, parameters, val_body);
         }
     }
-    auto r = m_elaborator(id, pre_type, pre_val);
+    auto r = elaborate(id, pre_type, pre_val);
     expr type = std::get<0>(r);
     expr val  = std::get<1>(r);
     metavar_env menv = std::get<2>(r);
@@ -212,7 +212,7 @@ void parser_imp::parse_variable_core(bool is_var) {
         expr type_body = parse_expr();
         pre_type = mk_abstraction(expr_kind::Pi, parameters, type_body);
     }
-    auto p = m_elaborator(pre_type);
+    auto p = elaborate(pre_type);
     expr type = p.first;
     metavar_env menv = p.second;
     if (has_metavar(type))
@@ -273,7 +273,7 @@ void parser_imp::parse_axiom() {
 /** \brief Parse 'Eval' expr */
 void parser_imp::parse_eval() {
     next();
-    expr v = m_elaborator(parse_expr()).first;
+    expr v = elaborate(parse_expr()).first;
     normalizer norm(m_env);
     expr r = norm(v);
     regular(m_io_state) << r << endl;
@@ -360,7 +360,7 @@ void parser_imp::parse_print() {
         next();
         regular(m_io_state) << msg << endl;
     } else {
-        expr v = m_elaborator(parse_expr()).first;
+        expr v = elaborate(parse_expr()).first;
         regular(m_io_state) << v << endl;
     }
 }
@@ -368,7 +368,7 @@ void parser_imp::parse_print() {
 /** \brief Parse 'Check' expr */
 void parser_imp::parse_check() {
     next();
-    auto p = m_elaborator(parse_expr());
+    auto p = elaborate(parse_expr());
     check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
     expr v = p.first;
     expr t = type_check(v, m_env);
@@ -709,7 +709,7 @@ void parser_imp::parse_builtin() {
     expr type;
     if (curr_is_colon()) {
         next();
-        auto p = m_elaborator(parse_expr());
+        auto p = elaborate(parse_expr());
         check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration");
         type = p.first;
     } else {
@@ -717,7 +717,7 @@ void parser_imp::parse_builtin() {
         parse_var_decl_parameters(parameters);
         check_colon_next("invalid builtin declaration, ':' expected");
         expr type_body = parse_expr();
-        auto p = m_elaborator(mk_abstraction(expr_kind::Pi, parameters, type_body));
+        auto p = elaborate(mk_abstraction(expr_kind::Pi, parameters, type_body));
         check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
         type = p.first;
     }
diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp
index e5d317ca5..f41beee28 100644
--- a/src/frontends/lean/parser_imp.cpp
+++ b/src/frontends/lean/parser_imp.cpp
@@ -126,6 +126,14 @@ void parser_imp::parse_script(bool as_expr) {
 
 void parser_imp::parse_script_expr() { return parse_script(true); }
 
+std::pair<expr, metavar_env> parser_imp::elaborate(expr const & e) {
+    return m_elaborator(e, m_io_state.get_options());
+}
+
+std::tuple<expr, expr, metavar_env> parser_imp::elaborate(name const & n, expr const & t, expr const & e) {
+    return m_elaborator(n, t, e, m_io_state.get_options());
+}
+
 void parser_imp::sync_command() {
     // Keep consuming tokens until we find a Command or End-of-file
     show_prompt();
@@ -217,7 +225,7 @@ bool parser_imp::parse_commands() {
 /** \brief Parse an expression. */
 expr parser_imp::parse_expr_main() {
     try {
-        auto p = m_elaborator(parse_expr());
+        auto p = elaborate(parse_expr());
         check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
         return p.first;
     } catch (parser_error & ex) {
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index e7e6e6621..4504f5264 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -242,6 +242,15 @@ private:
     void parse_script(bool as_expr = false);
     void parse_script_expr();
 
+    /**
+       @name Elaborator interface
+    */
+    /*@{*/
+private:
+    std::pair<expr, metavar_env> elaborate(expr const & e);
+    std::tuple<expr, expr, metavar_env> elaborate(name const & n, expr const & t, expr const & e);
+    /*@}*/
+
 
     /**
        @name Parse Universe levels
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 6a00621f7..aaf59d26b 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/list.h"
 #include "util/splay_tree.h"
 #include "util/interrupt.h"
+#include "util/sstream.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/formatter.h"
 #include "kernel/free_vars.h"
@@ -25,9 +26,40 @@ Author: Leonardo de Moura
 #include "library/elaborator/elaborator.h"
 #include "library/elaborator/elaborator_justification.h"
 
+#ifndef LEAN_ELABORATOR_MAX_STEPS
+#define LEAN_ELABORATOR_MAX_STEPS 100000
+#endif
+
+#ifndef LEAN_ELABORATOR_USE_NORMALIZER
+#define LEAN_ELABORATOR_USE_NORMALIZER true
+#endif
+
+#ifndef LEAN_ELABORATOR_INJECTIVITY
+#define LEAN_ELABORATOR_INJECTIVITY true
+#endif
+
 namespace lean {
 static name g_x_name("x");
 
+static name g_elaborator_max_steps      {"elaborator", "max_steps"};
+static name g_elaborator_use_normalizer {"elaborator", "use_normalizer"};
+static name g_elaborator_injectivity    {"elaborator", "injectivity"};
+
+RegisterUnsignedOption(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS, "(elaborator) maximum number of steps");
+RegisterBoolOption(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER,
+                   "(elaborator) invoke normalizer during elaboration");
+RegisterBoolOption(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY, "(elaborator) reduce unification constrainst of the form f(t1, t2) ≈ f(s1, s2)  into t1 ≈ s1 and t2 ≈ s2 even if f-applications are not in head normal form");
+
+unsigned get_elaborator_max_steps(options const & opts) {
+    return opts.get_unsigned(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS);
+}
+bool get_elaborator_use_normalizer(options const & opts) {
+    return opts.get_bool(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER);
+}
+bool get_elaborator_injectivity(options const & opts) {
+    return opts.get_bool(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY);
+}
+
 class elaborator::imp {
     typedef splay_tree<name, name_cmp>                         name_set;
     typedef list<unification_constraint>                       cnstr_list;
@@ -148,16 +180,26 @@ class elaborator::imp {
     justification                            m_conflict;
     bool                                     m_first;
     level                                    m_U; // universe U used for builtin kernel axioms
+    unsigned                                 m_num_steps;
 
     // options
     bool                                     m_use_justifications;
     bool                                     m_use_normalizer;
     bool                                     m_assume_injectivity;
+    unsigned                                 m_max_steps;
 
-    void set_options(options const &) {
+    void set_options(options const & o) {
         m_use_justifications = true;
-        m_use_normalizer     = true;
-        m_assume_injectivity = true;
+        m_use_normalizer     = get_elaborator_use_normalizer(o);
+        m_assume_injectivity = get_elaborator_injectivity(o);
+        m_max_steps          = get_elaborator_max_steps(o);
+    }
+
+    void check_system() {
+        check_interrupted();
+        if (m_num_steps > m_max_steps)
+            throw exception(sstream() << "elaborator maximum number of steps (" << m_max_steps << ") exceeded, the maximum number of steps can be increased by setting the option elaborator::max_steps (remark: the elaborator uses higher order unification, which may trigger non-termination");
+        m_num_steps++;
     }
 
     justification mk_assumption() {
@@ -683,7 +725,7 @@ class elaborator::imp {
         context const & ctx = get_context(c);
         bool modified = false;
         while (true) {
-            check_interrupted();
+            check_system();
             expr new_a = normalize_step(ctx, a);
             expr new_b = normalize_step(ctx, b);
             if (new_a == a && new_b == b) {
@@ -1899,11 +1941,13 @@ public:
         m_next_id     = 0;
         m_first       = true;
         m_U           = m_env->get_uvar("U");
+        m_num_steps   = 0;
         // display(std::cout);
     }
 
     metavar_env next() {
-        check_interrupted();
+        m_num_steps = 0;
+        check_system();
         if (m_conflict)
             throw elaborator_exception(m_conflict);
         if (!m_case_splits.empty()) {
@@ -1920,7 +1964,7 @@ public:
             throw elaborator_exception(m_conflict);
         }
         while (true) {
-            check_interrupted();
+            check_system();
             cnstr_list & active_cnstrs = m_state.m_active_cnstrs;
             if (!empty(active_cnstrs)) {
                 unification_constraint c = head(active_cnstrs);