From 9df712581bc0740b87ff2491281fc0dc39b1670e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Sep 2016 08:32:37 -0700
Subject: [PATCH] chore(frontends/lean): remove 'new_elaborator' option

---
 library/init/alternative.lean                         | 1 -
 library/init/applicative.lean                         | 1 -
 library/init/bool.lean                                | 1 -
 library/init/char.lean                                | 1 -
 library/init/classical.lean                           | 1 -
 library/init/coe.lean                                 | 1 -
 library/init/combinator.lean                          | 1 -
 library/init/datatypes.lean                           | 1 -
 library/init/fin.lean                                 | 1 -
 library/init/function.lean                            | 1 -
 library/init/functor.lean                             | 1 -
 library/init/funext.lean                              | 1 -
 library/init/id_locked.lean                           | 1 -
 library/init/instances.lean                           | 1 -
 library/init/list.lean                                | 1 -
 library/init/list_classes.lean                        | 1 -
 library/init/logic.lean                               | 1 -
 library/init/monad.lean                               | 1 -
 library/init/monad_combinators.lean                   | 1 -
 library/init/nat.lean                                 | 1 -
 library/init/nat_div.lean                             | 1 -
 library/init/num.lean                                 | 1 -
 library/init/option.lean                              | 1 -
 library/init/ordering.lean                            | 1 -
 library/init/prod.lean                                | 1 -
 library/init/quot.lean                                | 1 -
 library/init/relation.lean                            | 1 -
 library/init/setoid.lean                              | 1 -
 library/init/sigma.lean                               | 1 -
 library/init/state.lean                               | 1 -
 library/init/string.lean                              | 1 -
 library/init/subtype.lean                             | 1 -
 library/init/sum.lean                                 | 1 -
 library/init/timeit.lean                              | 1 -
 library/init/to_string.lean                           | 1 -
 library/init/trace.lean                               | 1 -
 library/init/unit.lean                                | 1 -
 library/init/unsigned.lean                            | 1 -
 src/frontends/lean/parser.cpp                         | 9 ---------
 src/frontends/lean/parser.h                           | 3 ---
 tests/lean/584a.lean                                  | 1 -
 tests/lean/634d.lean                                  | 1 -
 tests/lean/attribute_bug1.lean                        | 1 -
 tests/lean/attribute_bug1.lean.expected.out           | 4 ++--
 tests/lean/attributes.lean                            | 1 -
 tests/lean/attributes.lean.expected.out               | 4 ++--
 tests/lean/aux_decl_zeta.lean                         | 1 -
 tests/lean/aux_decl_zeta.lean.expected.out            | 2 +-
 tests/lean/bad_inaccessible.lean                      | 1 -
 tests/lean/bad_inaccessible.lean.expected.out         | 6 +++---
 tests/lean/bad_inaccessible2.lean                     | 1 -
 tests/lean/bad_inaccessible2.lean.expected.out        | 2 +-
 tests/lean/by_contradiction.lean                      | 1 -
 tests/lean/by_contradiction.lean.expected.out         | 2 +-
 tests/lean/caching_user_attribute.lean                | 1 -
 tests/lean/choice_expl.lean                           | 1 -
 tests/lean/choice_expl.lean.expected.out              | 2 +-
 tests/lean/config.lean                                | 1 -
 tests/lean/def1.lean                                  | 1 -
 tests/lean/def1.lean.expected.out                     | 2 +-
 tests/lean/def2.lean                                  | 1 -
 tests/lean/def2.lean.expected.out                     | 4 ++--
 tests/lean/def3.lean                                  | 1 -
 tests/lean/def4.lean                                  | 1 -
 tests/lean/def4.lean.expected.out                     | 4 ++--
 tests/lean/def_inaccessible_issue.lean                | 1 -
 tests/lean/def_ite_value.lean                         | 1 -
 tests/lean/elab15.lean                                | 1 -
 tests/lean/elab_meta2.lean                            | 1 -
 tests/lean/eqn_compiler_loop.lean                     | 1 -
 tests/lean/eqn_compiler_loop.lean.expected.out        | 2 +-
 tests/lean/eqn_hole.lean                              | 1 -
 tests/lean/eqn_hole.lean.expected.out                 | 4 ++--
 tests/lean/eqn_sanitizer1.lean                        | 1 -
 tests/lean/hole_in_fn.lean                            | 1 -
 tests/lean/hole_in_fn.lean.expected.out               | 2 +-
 tests/lean/hole_issue2.lean                           | 1 -
 tests/lean/hole_issue2.lean.expected.out              | 6 +++---
 tests/lean/inaccessible2.lean                         | 1 -
 tests/lean/inaccessible2.lean.expected.out            | 8 ++++----
 tests/lean/inst.lean                                  | 1 -
 tests/lean/instance_cache1.lean                       | 1 -
 tests/lean/instance_cache1.lean.expected.out          | 6 +++---
 tests/lean/let1.lean                                  | 1 -
 tests/lean/let1.lean.expected.out                     | 2 +-
 tests/lean/let3.lean                                  | 1 -
 tests/lean/let4.lean                                  | 1 -
 tests/lean/non_exhaustive_error.lean                  | 1 -
 tests/lean/non_exhaustive_error.lean.expected.out     | 2 +-
 tests/lean/print_ax3.lean                             | 1 -
 tests/lean/red.lean                                   | 1 -
 tests/lean/red.lean.expected.out                      | 6 +++---
 tests/lean/run/662.lean                               | 1 -
 tests/lean/run/K_new_elab.lean                        | 1 -
 tests/lean/run/assoc_flat.lean                        | 1 -
 tests/lean/run/at_at_bug.lean                         | 1 -
 tests/lean/run/basic.lean                             | 1 -
 tests/lean/run/cases_bug3.lean                        | 1 -
 tests/lean/run/cases_tac1.lean                        | 1 -
 tests/lean/run/choice_ctx.lean                        | 1 -
 tests/lean/run/class1.lean                            | 1 -
 tests/lean/run/class2.lean                            | 1 -
 tests/lean/run/class3.lean                            | 1 -
 tests/lean/run/class6.lean                            | 1 -
 tests/lean/run/const_choice.lean                      | 1 -
 tests/lean/run/contra3.lean                           | 1 -
 tests/lean/run/dec_trivial_problem.lean               | 1 -
 tests/lean/run/def1.lean                              | 1 -
 tests/lean/run/def10.lean                             | 1 -
 tests/lean/run/def11.lean                             | 1 -
 tests/lean/run/def12.lean                             | 1 -
 tests/lean/run/def13.lean                             | 1 -
 tests/lean/run/def2.lean                              | 1 -
 tests/lean/run/def3.lean                              | 1 -
 tests/lean/run/def4.lean                              | 1 -
 tests/lean/run/def5.lean                              | 1 -
 tests/lean/run/def6.lean                              | 1 -
 tests/lean/run/def7.lean                              | 1 -
 tests/lean/run/def8.lean                              | 1 -
 tests/lean/run/def9.lean                              | 1 -
 tests/lean/run/def_alias.lean                         | 1 -
 tests/lean/run/def_brec1.lean                         | 1 -
 tests/lean/run/def_brec2.lean                         | 1 -
 tests/lean/run/def_brec3.lean                         | 1 -
 tests/lean/run/def_brec4.lean                         | 1 -
 tests/lean/run/def_brec_reflexive.lean                | 1 -
 tests/lean/run/def_complete_bug.lean                  | 1 -
 tests/lean/run/def_ite1.lean                          | 1 -
 tests/lean/run/def_ite_value.lean                     | 1 -
 tests/lean/run/div_wf.lean                            | 1 -
 tests/lean/run/e4.lean                                | 1 -
 tests/lean/run/elab_meta1.lean                        | 1 -
 tests/lean/run/empty_eq.lean                          | 1 -
 tests/lean/run/empty_match.lean                       | 1 -
 tests/lean/run/empty_match_bug.lean                   | 1 -
 tests/lean/run/eq1.lean                               | 1 -
 tests/lean/run/eq10.lean                              | 1 -
 tests/lean/run/eq11.lean                              | 1 -
 tests/lean/run/eq12.lean                              | 1 -
 tests/lean/run/eq13.lean                              | 1 -
 tests/lean/run/eq15.lean                              | 1 -
 tests/lean/run/eq16.lean                              | 1 -
 tests/lean/run/eq17.lean                              | 1 -
 tests/lean/run/eq2.lean                               | 1 -
 tests/lean/run/eq20.lean                              | 1 -
 tests/lean/run/eq21.lean                              | 1 -
 tests/lean/run/eq22.lean                              | 1 -
 tests/lean/run/eq25.lean                              | 1 -
 tests/lean/run/eq4.lean                               | 1 -
 tests/lean/run/eq5.lean                               | 1 -
 tests/lean/run/eq6.lean                               | 1 -
 tests/lean/run/eq9.lean                               | 1 -
 tests/lean/run/exists_intro1.lean                     | 1 -
 tests/lean/run/fib_wrec.lean                          | 1 -
 tests/lean/run/interp.lean                            | 1 -
 tests/lean/run/let1.lean                              | 1 -
 tests/lean/run/let2.lean                              | 1 -
 tests/lean/run/let3.lean                              | 1 -
 tests/lean/run/lift_nested_rec.lean                   | 1 -
 tests/lean/run/match3.lean                            | 1 -
 tests/lean/run/match_anonymous_constructor.lean       | 1 -
 tests/lean/run/match_convoy2.lean                     | 1 -
 tests/lean/run/match_convoy3.lean                     | 1 -
 tests/lean/run/match_fun.lean                         | 1 -
 tests/lean/run/match_pattern2.lean                    | 1 -
 tests/lean/run/meta2.lean                             | 1 -
 tests/lean/run/meta_tac1.lean                         | 1 -
 tests/lean/run/nat_bug.lean                           | 1 -
 tests/lean/run/nat_bug4.lean                          | 1 -
 tests/lean/run/nat_bug7.lean                          | 1 -
 tests/lean/run/new_elab1.lean                         | 1 -
 tests/lean/run/new_elab2.lean                         | 1 -
 tests/lean/run/no_confusion1.lean                     | 1 -
 tests/lean/run/occurs_check_bug1.lean                 | 1 -
 tests/lean/run/over_subst.lean                        | 1 -
 tests/lean/run/overload_issue.lean                    | 1 -
 tests/lean/run/pack_unpack1.lean                      | 1 -
 tests/lean/run/pack_unpack2.lean                      | 1 -
 tests/lean/run/pack_unpack3.lean                      | 1 -
 tests/lean/run/parent_struct_inst.lean                | 1 -
 tests/lean/run/section4.lean                          | 1 -
 tests/lean/run/section_var_bug.lean                   | 1 -
 tests/lean/run/set_attr1.lean                         | 1 -
 tests/lean/run/sigma_match.lean                       | 1 -
 tests/lean/run/simplifier_canonize_instances.lean     | 1 -
 tests/lean/run/simplifier_canonize_subsingletons.lean | 1 -
 tests/lean/run/stateT1.lean                           | 1 -
 tests/lean/run/sufficies.lean                         | 1 -
 tests/lean/run/t4.lean                                | 1 -
 tests/lean/run/t6.lean                                | 1 -
 tests/lean/run/test_single.sh                         | 2 +-
 tests/lean/run/unfold_crash.lean                      | 1 -
 tests/lean/run/uni_issue1.lean                        | 1 -
 tests/lean/run/whnfinst.lean                          | 1 -
 tests/lean/sec_param_pp.lean                          | 1 -
 tests/lean/set_attr1.lean                             | 1 -
 tests/lean/set_attr1.lean.expected.out                | 2 +-
 tests/lean/synth_inferred_mismatch.lean               | 1 -
 tests/lean/synth_inferred_mismatch.lean.expected.out  | 2 +-
 tests/lean/tuple.lean                                 | 1 -
 tests/lean/user_attribute.lean                        | 1 -
 tests/lean/user_attribute.lean.expected.out           | 6 +++---
 tests/lean/wrong_arity.lean                           | 1 -
 tests/lean/wrong_arity.lean.expected.out              | 2 +-
 204 files changed, 42 insertions(+), 232 deletions(-)
 mode change 100755 => 100644 tests/lean/run/test_single.sh

diff --git a/library/init/alternative.lean b/library/init/alternative.lean
index f3692a399a..5624e61cb3 100644
--- a/library/init/alternative.lean
+++ b/library/init/alternative.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.logic init.applicative
-set_option new_elaborator true
 universe variables u v
 
 structure [class] alternative (F : Type u → Type v) extends applicative F : Type (max u+1 v) :=
diff --git a/library/init/applicative.lean b/library/init/applicative.lean
index 448be6f5a8..1412751ceb 100644
--- a/library/init/applicative.lean
+++ b/library/init/applicative.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.functor
-set_option new_elaborator true
 universe variables u v
 
 structure [class] applicative (F : Type u → Type v) extends functor F : Type (max u+1 v):=
diff --git a/library/init/bool.lean b/library/init/bool.lean
index 24528510d8..ec55b2ffd6 100644
--- a/library/init/bool.lean
+++ b/library/init/bool.lean
@@ -3,7 +3,6 @@
 -- Author: Leonardo de Moura
 prelude
 import init.datatypes
-set_option new_elaborator true
 
 namespace bool
   attribute [inline]
diff --git a/library/init/char.lean b/library/init/char.lean
index eb3a36fda3..f9654c3c0a 100644
--- a/library/init/char.lean
+++ b/library/init/char.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.fin
-set_option new_elaborator true
 
 open nat
 definition char_sz : nat := succ 255
diff --git a/library/init/classical.lean b/library/init/classical.lean
index d911d8708f..afad3988d1 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
 import init.subtype init.funext
-set_option new_elaborator true
 namespace classical
 open subtype
 universe variables u v
diff --git a/library/init/coe.lean b/library/init/coe.lean
index c3c014e6cf..fed1f98bfd 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -25,7 +25,6 @@ a type to a sort.
 -/
 prelude
 import init.list init.subtype init.prod
-set_option new_elaborator true
 universe variables u v
 
 structure [class] has_lift (A : Type u) (B : Type v) :=
diff --git a/library/init/combinator.lean b/library/init/combinator.lean
index 1c5be3f173..cfcd1535bb 100644
--- a/library/init/combinator.lean
+++ b/library/init/combinator.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-set_option new_elaborator true
 /- Combinator calculus -/
 namespace combinator
 universe variables u₁ u₂ u₃
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 07ddaf37fb..557a146ace 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 Basic datatypes
 -/
 prelude
-set_option new_elaborator true
 
 notation `Prop`  := Type 0
 notation `Type₂` := Type 2
diff --git a/library/init/fin.lean b/library/init/fin.lean
index 1f289455eb..36a14fff59 100644
--- a/library/init/fin.lean
+++ b/library/init/fin.lean
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 prelude
 import init.nat
 open nat
-set_option new_elaborator true
 structure fin (n : nat) := (val : nat) (is_lt : val < n)
 
 namespace fin
diff --git a/library/init/function.lean b/library/init/function.lean
index 5da0a5797d..e43ee743f7 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -7,7 +7,6 @@ General operations on functions.
 -/
 prelude
 import init.prod init.funext init.logic
-set_option new_elaborator true
 notation f ` $ `:1 a:1 := f a
 universe variables u_a u_b u_c u_d u_e
 variables {A : Type u_a} {B : Type u_b} {C : Type u_c} {D : Type u_d} {E : Type u_a}
diff --git a/library/init/functor.lean b/library/init/functor.lean
index 5ccea24b65..cb845e9f9b 100644
--- a/library/init/functor.lean
+++ b/library/init/functor.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson and Jared Roesch
 -/
 prelude
-set_option new_elaborator true
 universe variables u v
 
 structure [class] functor (F : Type u → Type v) : Type (max u+1 v) :=
diff --git a/library/init/funext.lean b/library/init/funext.lean
index 5a4fee4206..d487d4a4d3 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -7,7 +7,6 @@ Extensional equality for functions, and a proof of function extensionality from
 -/
 prelude
 import init.quot init.logic
-set_option new_elaborator true
 
 namespace function
   universe variables u v
diff --git a/library/init/id_locked.lean b/library/init/id_locked.lean
index 2cbb638c8a..8bdb06fe91 100644
--- a/library/init/id_locked.lean
+++ b/library/init/id_locked.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.tactic init.meta.constructor_tactic
 open tactic
-set_option new_elaborator true
 /-
   Define id_locked using meta-programming because we don't have
   syntax for setting reducibility_hints.
diff --git a/library/init/instances.lean b/library/init/instances.lean
index 9d395c51a2..be36d14555 100644
--- a/library/init/instances.lean
+++ b/library/init/instances.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences init.sum
-set_option new_elaborator true
 open tactic subtype
 universe variables u v
 
diff --git a/library/init/list.lean b/library/init/list.lean
index 80492db1c8..919ed66ac4 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 prelude
 import init.logic init.nat
 open decidable list
-set_option new_elaborator true
 
 universe variables u v
 
diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean
index 02da3d9824..d8d6ea39c8 100644
--- a/library/init/list_classes.lean
+++ b/library/init/list_classes.lean
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 prelude
 import init.monad init.alternative
 open list
-set_option new_elaborator true
 universe variables u v
 attribute [inline]
 definition list_fmap {A : Type u} {B : Type v} (f : A → B) (l : list A) : list B :=
diff --git a/library/init/logic.lean b/library/init/logic.lean
index aa2fc5c863..49746b5901 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
 import init.datatypes
-set_option new_elaborator true
 
 universe variables u v
 
diff --git a/library/init/monad.lean b/library/init/monad.lean
index 9eb2d989f6..1fbf1be534 100644
--- a/library/init/monad.lean
+++ b/library/init/monad.lean
@@ -5,7 +5,6 @@ Authors: Luke Nelson and Jared Roesch
 -/
 prelude
 import init.applicative init.string init.trace
-set_option new_elaborator true
 universe variables u v
 
 structure [class] monad (M : Type u → Type v) extends functor M : Type (max u+1 v) :=
diff --git a/library/init/monad_combinators.lean b/library/init/monad_combinators.lean
index a08298d1c6..5cbbb63ac7 100644
--- a/library/init/monad_combinators.lean
+++ b/library/init/monad_combinators.lean
@@ -7,7 +7,6 @@ Monad combinators, as in Haskell's Control.Monad.
 -/
 prelude
 import init.monad init.list
-set_option new_elaborator true
 namespace monad
 
 definition mapM {m : Type → Type} [monad m] {A B : Type} (f : A → m B) : list A → m (list B)
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 9c5cd74e79..3888f8aa16 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -5,7 +5,6 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import init.relation init.num
-set_option new_elaborator true
 
 notation `ℕ` := nat
 
diff --git a/library/init/nat_div.lean b/library/init/nat_div.lean
index 8acf1a7442..2f2e0f3f2b 100644
--- a/library/init/nat_div.lean
+++ b/library/init/nat_div.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.wf init.nat
-set_option new_elaborator true
 namespace nat
 
 private definition div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x :=
diff --git a/library/init/num.lean b/library/init/num.lean
index 5f494d351a..a13fc16b28 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.bool
-set_option new_elaborator true
 
 namespace pos_num
   protected definition mul (a b : pos_num) : pos_num :=
diff --git a/library/init/option.lean b/library/init/option.lean
index c0d9e9523f..a926493c3e 100644
--- a/library/init/option.lean
+++ b/library/init/option.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic init.monad init.alternative
-set_option new_elaborator true
 open decidable
 
 universe variables u v
diff --git a/library/init/ordering.lean b/library/init/ordering.lean
index d25b77547d..e9ed163480 100644
--- a/library/init/ordering.lean
+++ b/library/init/ordering.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.to_string init.prod init.sum
-set_option new_elaborator true
 
 inductive ordering
 | lt | eq | gt
diff --git a/library/init/prod.lean b/library/init/prod.lean
index 1a28d90edd..4fee1b1086 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
 import init.num init.relation
-set_option new_elaborator true
 notation A × B := prod A B
 -- notation for n-ary tuples
 notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t
diff --git a/library/init/quot.lean b/library/init/quot.lean
index 83c632c908..52b96ca0e8 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -8,7 +8,6 @@ Quotient types.
 prelude
 import init.sigma init.setoid init.logic
 open sigma.ops setoid
-set_option new_elaborator true
 
 universe variables u v
 
diff --git a/library/init/relation.lean b/library/init/relation.lean
index d32e02614d..1ff0e56e90 100644
--- a/library/init/relation.lean
+++ b/library/init/relation.lean
@@ -7,7 +7,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic
-set_option new_elaborator true
 
 -- TODO(Leo): remove duplication between this file and algebra/relation.lean
 -- We need some of the following definitions asap when "initializing" Lean.
diff --git a/library/init/setoid.lean b/library/init/setoid.lean
index 2257f0646c..61e4b3407d 100644
--- a/library/init/setoid.lean
+++ b/library/init/setoid.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.relation
-set_option new_elaborator true
 universe variables u
 structure [class] setoid (A : Type u) :=
 (r : A → A → Prop) (iseqv : equivalence r)
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index ab10797f95..82961d6349 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
 import init.datatypes init.num init.wf init.logic
-set_option new_elaborator true
 
 definition dpair := @sigma.mk
 notation `Σ` binders `, ` r:(scoped P, sigma P) := r
diff --git a/library/init/state.lean b/library/init/state.lean
index 84192de9e4..08ed7347c1 100644
--- a/library/init/state.lean
+++ b/library/init/state.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic init.monad init.alternative init.prod
-set_option new_elaborator true
 
 definition state (S : Type) (A : Type) : Type :=
 S → A × S
diff --git a/library/init/string.lean b/library/init/string.lean
index fc02793efa..b9b536a732 100644
--- a/library/init/string.lean
+++ b/library/init/string.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.char init.list
-set_option new_elaborator true
 attribute [reducible]
 definition string := list char
 
diff --git a/library/init/subtype.lean b/library/init/subtype.lean
index b809ac92e4..6bd3b6e6b4 100644
--- a/library/init/subtype.lean
+++ b/library/init/subtype.lean
@@ -6,7 +6,6 @@ Author: Leonardo de Moura, Jeremy Avigad
 prelude
 import init.datatypes init.logic
 open decidable
-set_option new_elaborator true
 
 universe variables u
 
diff --git a/library/init/sum.lean b/library/init/sum.lean
index 555d98dfc7..5bcdc1c424 100644
--- a/library/init/sum.lean
+++ b/library/init/sum.lean
@@ -7,7 +7,6 @@ The sum type, aka disjoint union.
 -/
 prelude
 import init.logic
-set_option new_elaborator true
 
 notation A ⊕ B := sum A B
 
diff --git a/library/init/timeit.lean b/library/init/timeit.lean
index eb7b18c97b..0d44b5674b 100644
--- a/library/init/timeit.lean
+++ b/library/init/timeit.lean
@@ -3,7 +3,6 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string
-set_option new_elaborator true
 
 /- This function has a native implementation that tracks time. -/
 definition timeit {A : Type} (s : string) (f : unit → A) : A :=
diff --git a/library/init/to_string.lean b/library/init/to_string.lean
index f00dec8084..4301cfed3a 100644
--- a/library/init/to_string.lean
+++ b/library/init/to_string.lean
@@ -3,7 +3,6 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string init.bool init.subtype init.unsigned init.prod init.sum
-set_option new_elaborator true
 open bool list sum prod sigma subtype nat
 
 universe variables u v
diff --git a/library/init/trace.lean b/library/init/trace.lean
index bfa4f87187..9519ec16e6 100644
--- a/library/init/trace.lean
+++ b/library/init/trace.lean
@@ -3,7 +3,6 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string
-set_option new_elaborator true
 
 /- This function has a native implementation that displays the given string in the regular output stream. -/
 definition trace {A : Type} (s : string) (f : unit → A) : A :=
diff --git a/library/init/unit.lean b/library/init/unit.lean
index b372273b6d..8a69ec30ab 100644
--- a/library/init/unit.lean
+++ b/library/init/unit.lean
@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.logic
-set_option new_elaborator true
 
 theorem unit_eq (a b : unit) : a = b :=
 unit.rec_on a (unit.rec_on b rfl)
diff --git a/library/init/unsigned.lean b/library/init/unsigned.lean
index b661f437a3..6f84808582 100644
--- a/library/init/unsigned.lean
+++ b/library/init/unsigned.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.fin
-set_option new_elaborator true
 
 open nat
 definition unsigned_sz : nat := succ 4294967295
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 77fafadc3b..d26147c9ce 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -75,7 +75,6 @@ namespace lean {
 // Parser configuration options
 static name * g_parser_show_errors;
 static name * g_parser_parallel_import;
-static name * g_new_elaborator;
 
 bool get_parser_show_errors(options const & opts) {
     return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS);
@@ -84,10 +83,6 @@ bool get_parser_show_errors(options const & opts) {
 bool get_parser_parallel_import(options const & opts) {
     return opts.get_bool(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT);
 }
-
-bool get_new_elaborator(options const & opts) {
-    return opts.get_bool(*g_new_elaborator, true);
-}
 // ==========================================
 
 static name * g_anonymous_inst_name_prefix = nullptr;
@@ -321,7 +316,6 @@ void parser::declare_sorry() {
 void parser::updt_options() {
     m_verbose        = get_verbose(m_ios.get_options());
     m_show_errors    = get_parser_show_errors(m_ios.get_options());
-    m_new_elaborator = get_new_elaborator(m_ios.get_options());
     try {
         set_max_memory_megabyte(get_max_memory(m_ios.get_options()));
     } catch (exception&) {
@@ -2355,12 +2349,10 @@ bool parse_commands(environment & env, io_state & ios, char const * fname, optio
 void initialize_parser() {
     g_parser_show_errors     = new name{"parser", "show_errors"};
     g_parser_parallel_import = new name{"parser", "parallel_import"};
-    g_new_elaborator         = new name{"new_elaborator"};
     register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
                          "(lean parser) display error messages in the regular output channel");
     register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
                          "(lean parser) import modules in parallel");
-    register_bool_option(*g_new_elaborator, false, "(lean parser) use new elaborator");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     g_anonymous_inst_name_prefix = new name("_inst");
 }
@@ -2370,6 +2362,5 @@ void finalize_parser() {
     delete g_tmp_prefix;
     delete g_parser_show_errors;
     delete g_parser_parallel_import;
-    delete g_new_elaborator;
 }
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index d928427523..6ce3bfa53a 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -234,9 +234,6 @@ public:
 
     cmd_table const & cmds() const { return get_cmd_table(env()); }
 
-    /* TODO(Leo): delete after we finish the transition to new elaborator */
-    bool use_new_elaborator() const { return m_new_elaborator; }
-
     void set_cache(definition_cache * c) { m_cache = c; }
     void cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                           level_param_names const & ls, expr const & type, expr const & value, bool is_trusted);
diff --git a/tests/lean/584a.lean b/tests/lean/584a.lean
index 0fe38a0122..a16e38e71f 100644
--- a/tests/lean/584a.lean
+++ b/tests/lean/584a.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variables u
 variables (A : Type u) [H : inhabited A] (x : A)
 include H
diff --git a/tests/lean/634d.lean b/tests/lean/634d.lean
index 82ffd3f4b6..cbc2d7b0d0 100644
--- a/tests/lean/634d.lean
+++ b/tests/lean/634d.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true open nat
 section
   universe l
   definition A {n : ℕ} (t : Type l) := t
diff --git a/tests/lean/attribute_bug1.lean b/tests/lean/attribute_bug1.lean
index 7dbaed7453..a85e401654 100644
--- a/tests/lean/attribute_bug1.lean
+++ b/tests/lean/attribute_bug1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 constant f    : nat → nat
diff --git a/tests/lean/attribute_bug1.lean.expected.out b/tests/lean/attribute_bug1.lean.expected.out
index 52534ccdd8..28f5ecd1fe 100644
--- a/tests/lean/attribute_bug1.lean.expected.out
+++ b/tests/lean/attribute_bug1.lean.expected.out
@@ -1,9 +1,9 @@
-attribute_bug1.lean:8:0: error: simp tactic failed to simplify
+attribute_bug1.lean:7:0: error: simp tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1
 constant fdef : ∀ (n : ℕ), f n = n + 1
-attribute_bug1.lean:20:0: error: simp tactic failed to simplify
+attribute_bug1.lean:19:0: error: simp tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1
diff --git a/tests/lean/attributes.lean b/tests/lean/attributes.lean
index f420da634d..a221f0e52a 100644
--- a/tests/lean/attributes.lean
+++ b/tests/lean/attributes.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variables u
 definition foo (A : Type u) := A
 
diff --git a/tests/lean/attributes.lean.expected.out b/tests/lean/attributes.lean.expected.out
index 6f4f37e9d7..ab5ab01360 100644
--- a/tests/lean/attributes.lean.expected.out
+++ b/tests/lean/attributes.lean.expected.out
@@ -1,2 +1,2 @@
-attributes.lean:6:0: error: cannot remove attribute [reducible]
-attributes.lean:10:0: error: cannot remove attribute [instance]
+attributes.lean:5:0: error: cannot remove attribute [reducible]
+attributes.lean:9:0: error: cannot remove attribute [instance]
diff --git a/tests/lean/aux_decl_zeta.lean b/tests/lean/aux_decl_zeta.lean
index 817e14b3d1..ea4cf2479e 100644
--- a/tests/lean/aux_decl_zeta.lean
+++ b/tests/lean/aux_decl_zeta.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type*) : nat → Type*
 | nil  : vec 0
diff --git a/tests/lean/aux_decl_zeta.lean.expected.out b/tests/lean/aux_decl_zeta.lean.expected.out
index 63a9e3f3ee..0c610a8246 100644
--- a/tests/lean/aux_decl_zeta.lean.expected.out
+++ b/tests/lean/aux_decl_zeta.lean.expected.out
@@ -1,4 +1,4 @@
-aux_decl_zeta.lean:7:0: error: equation compiler failed to create auxiliary declaration 'f._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
+aux_decl_zeta.lean:6:0: error: equation compiler failed to create auxiliary declaration 'f._match_1', auxiliary declaration has references to let-declarations (possible solution: use 'set_option eqn_compiler.zeta true')
 nested exception message:
 type mismatch at application
   x = w
diff --git a/tests/lean/bad_inaccessible.lean b/tests/lean/bad_inaccessible.lean
index 4b41329aa4..b3705fba61 100644
--- a/tests/lean/bad_inaccessible.lean
+++ b/tests/lean/bad_inaccessible.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variables u
 definition f : nat → nat → nat
 | a .a := a
diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out
index c1391f5dc3..2bfa2331f3 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,7 +1,7 @@
-bad_inaccessible.lean:4:5: error: invalid use of inaccessible term, it is not fixed by other arguments
-bad_inaccessible.lean:7:7: error: invalid use of inaccessible term, the provided term is
+bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
+bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
   b
 but is expected to be
   a
-bad_inaccessible.lean:15:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
+bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
diff --git a/tests/lean/bad_inaccessible2.lean b/tests/lean/bad_inaccessible2.lean
index 6cd8de2033..f288ddeb14 100644
--- a/tests/lean/bad_inaccessible2.lean
+++ b/tests/lean/bad_inaccessible2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variables u
 inductive vec (A : Type u) : nat → Type (max 1 u)
 | nil {} : vec 0
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index d43f989714..dfbdf42e16 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -1,4 +1,4 @@
-bad_inaccessible2.lean:32:2: error: type mismatch at application
+bad_inaccessible2.lean:31:2: error: type mismatch at application
   map_head (cons a va) (cons b vb)
 term
   cons b vb
diff --git a/tests/lean/by_contradiction.lean b/tests/lean/by_contradiction.lean
index 91a15f0141..ea4f82d04a 100644
--- a/tests/lean/by_contradiction.lean
+++ b/tests/lean/by_contradiction.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true --
 open tactic nat
 
 example (a b : nat) : a ≠ b → ¬ a = b :=
diff --git a/tests/lean/by_contradiction.lean.expected.out b/tests/lean/by_contradiction.lean.expected.out
index 7bb0df1e48..3a1e7b6104 100644
--- a/tests/lean/by_contradiction.lean.expected.out
+++ b/tests/lean/by_contradiction.lean.expected.out
@@ -8,7 +8,7 @@ a_1 : ¬¬a = b,
 H : ¬a = b
 ⊢ false
 -------
-by_contradiction.lean:23:0: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
+by_contradiction.lean:22:0: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
 state:
 p q : Prop,
 a : ¬¬p
diff --git a/tests/lean/caching_user_attribute.lean b/tests/lean/caching_user_attribute.lean
index d2c0aa0adb..5e73ff6299 100644
--- a/tests/lean/caching_user_attribute.lean
+++ b/tests/lean/caching_user_attribute.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 definition foo_attr : caching_user_attribute :=
 ⟨`foo, "bar", string, list.join ∘ list.map (list.append "\n" ∘ to_string ∘ declaration.to_name) ⟩
 
diff --git a/tests/lean/choice_expl.lean b/tests/lean/choice_expl.lean
index c7750180c4..2a4d97e976 100644
--- a/tests/lean/choice_expl.lean
+++ b/tests/lean/choice_expl.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variables u
 namespace N1
   definition pr {A : Type u} (a b : A) := a
diff --git a/tests/lean/choice_expl.lean.expected.out b/tests/lean/choice_expl.lean.expected.out
index f861e790f5..44725fa7eb 100644
--- a/tests/lean/choice_expl.lean.expected.out
+++ b/tests/lean/choice_expl.lean.expected.out
@@ -1,5 +1,5 @@
 pr : Π {A : Type u_1}, A → A → A
 pr a b : N
-choice_expl.lean:16:6: error: ambiguous overload, possible interpretations
+choice_expl.lean:15:6: error: ambiguous overload, possible interpretations
   N2.pr a b
   N1.pr a b
diff --git a/tests/lean/config.lean b/tests/lean/config.lean
index 3fa931d9df..e900c86a6d 100644
--- a/tests/lean/config.lean
+++ b/tests/lean/config.lean
@@ -2,4 +2,3 @@
 prelude
 set_option pp.colors  false
 set_option pp.unicode true
-set_option new_elaborator true
diff --git a/tests/lean/def1.lean b/tests/lean/def1.lean
index 180752ada2..83156af66c 100644
--- a/tests/lean/def1.lean
+++ b/tests/lean/def1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variable u
 variable {A : Type u}
 
diff --git a/tests/lean/def1.lean.expected.out b/tests/lean/def1.lean.expected.out
index 537ed285a6..5f44ec03a1 100644
--- a/tests/lean/def1.lean.expected.out
+++ b/tests/lean/def1.lean.expected.out
@@ -1,4 +1,4 @@
-def1.lean:6:16: error: "eliminator" elaborator type mismatch, term
+def1.lean:5:16: error: "eliminator" elaborator type mismatch, term
   rfl
 has type
   ?m_2 = ?m_2
diff --git a/tests/lean/def2.lean b/tests/lean/def2.lean
index d4e5f50df6..d6777080bc 100644
--- a/tests/lean/def2.lean
+++ b/tests/lean/def2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 axiom val : nat
 
diff --git a/tests/lean/def2.lean.expected.out b/tests/lean/def2.lean.expected.out
index 5a93a91a45..65899f7c7a 100644
--- a/tests/lean/def2.lean.expected.out
+++ b/tests/lean/def2.lean.expected.out
@@ -1,2 +1,2 @@
-def2.lean:5:0: error: definition 'foo' is noncomputable, it depends on 'val'
-def2.lean:11:0: error: definition 'bla' was incorrectly marked as noncomputable
+def2.lean:4:0: error: definition 'foo' is noncomputable, it depends on 'val'
+def2.lean:10:0: error: definition 'bla' was incorrectly marked as noncomputable
diff --git a/tests/lean/def3.lean b/tests/lean/def3.lean
index 169f899fb9..d59832b285 100644
--- a/tests/lean/def3.lean
+++ b/tests/lean/def3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variable u
 section
   variable (A : Type u)
diff --git a/tests/lean/def4.lean b/tests/lean/def4.lean
index 36c09d9eed..9e7e262ac8 100644
--- a/tests/lean/def4.lean
+++ b/tests/lean/def4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 universe variable u
 section
   parameter (A : Type u)
diff --git a/tests/lean/def4.lean.expected.out b/tests/lean/def4.lean.expected.out
index b6632b2840..e12161f3a0 100644
--- a/tests/lean/def4.lean.expected.out
+++ b/tests/lean/def4.lean.expected.out
@@ -1,5 +1,5 @@
 f : A → A
-def4.lean:10:8: error: type mismatch at application
+def4.lean:9:8: error: type mismatch at application
   f 0
 term
   0
@@ -8,7 +8,7 @@ has type
 but is expected to have type
   A
 g : A → A
-def4.lean:18:8: error: type mismatch at application
+def4.lean:17:8: error: type mismatch at application
   g 0
 term
   0
diff --git a/tests/lean/def_inaccessible_issue.lean b/tests/lean/def_inaccessible_issue.lean
index af282fa60f..422e21a078 100644
--- a/tests/lean/def_inaccessible_issue.lean
+++ b/tests/lean/def_inaccessible_issue.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option eqn_compiler.dsimp true
 open nat
 
diff --git a/tests/lean/def_ite_value.lean b/tests/lean/def_ite_value.lean
index 2274710a42..6ec74e2dc9 100644
--- a/tests/lean/def_ite_value.lean
+++ b/tests/lean/def_ite_value.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option eqn_compiler.lemmas false -- TODO(Leo): remove
 definition f : string → nat → nat
 | "hello world" 1 := 0
diff --git a/tests/lean/elab15.lean b/tests/lean/elab15.lean
index ab73a22efe..9cda19b72e 100644
--- a/tests/lean/elab15.lean
+++ b/tests/lean/elab15.lean
@@ -1,5 +1,4 @@
 open tactic
-set_option new_elaborator true
 set_option pp.notation false
 universe variables u
 check
diff --git a/tests/lean/elab_meta2.lean b/tests/lean/elab_meta2.lean
index 4b85920b48..de48504adb 100644
--- a/tests/lean/elab_meta2.lean
+++ b/tests/lean/elab_meta2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 print "parametric meta_definition"
 meta_definition f {A : Type} : nat → A → A → A
diff --git a/tests/lean/eqn_compiler_loop.lean b/tests/lean/eqn_compiler_loop.lean
index b4c024538a..823ab3f7d9 100644
--- a/tests/lean/eqn_compiler_loop.lean
+++ b/tests/lean/eqn_compiler_loop.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 theorem succ_ne_self : ∀ (n : ℕ), succ n ≠ n
diff --git a/tests/lean/eqn_compiler_loop.lean.expected.out b/tests/lean/eqn_compiler_loop.lean.expected.out
index 9e9480709f..c40493c3c0 100644
--- a/tests/lean/eqn_compiler_loop.lean.expected.out
+++ b/tests/lean/eqn_compiler_loop.lean.expected.out
@@ -1 +1 @@
-eqn_compiler_loop.lean:4:8: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
+eqn_compiler_loop.lean:3:8: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/eqn_hole.lean b/tests/lean/eqn_hole.lean
index a58d984cdb..843772e021 100644
--- a/tests/lean/eqn_hole.lean
+++ b/tests/lean/eqn_hole.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f : nat → nat
 | 0 := _
diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out
index 76af8b10d5..7331e0d29b 100644
--- a/tests/lean/eqn_hole.lean.expected.out
+++ b/tests/lean/eqn_hole.lean.expected.out
@@ -1,8 +1,8 @@
-eqn_hole.lean:4:7: error: don't know how to synthesize placeholder
+eqn_hole.lean:3:7: error: don't know how to synthesize placeholder
 state:
 f : ℕ → ℕ
 ⊢ ℕ
-eqn_hole.lean:9:13: error: don't know how to synthesize placeholder
+eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
 state:
 g : ℕ → ℕ,
 n : ℕ
diff --git a/tests/lean/eqn_sanitizer1.lean b/tests/lean/eqn_sanitizer1.lean
index a137578a1a..e72a556174 100644
--- a/tests/lean/eqn_sanitizer1.lean
+++ b/tests/lean/eqn_sanitizer1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option eqn_compiler.dsimp true
 attribute [eqn_sanitizer]
 definition succ_eq (a : nat) : nat.succ a = a + 1 :=
diff --git a/tests/lean/hole_in_fn.lean b/tests/lean/hole_in_fn.lean
index 75756902ff..866aad72b9 100644
--- a/tests/lean/hole_in_fn.lean
+++ b/tests/lean/hole_in_fn.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive foo
 | mk : (nat → nat) → foo
diff --git a/tests/lean/hole_in_fn.lean.expected.out b/tests/lean/hole_in_fn.lean.expected.out
index 215249f3a4..96d7d28001 100644
--- a/tests/lean/hole_in_fn.lean.expected.out
+++ b/tests/lean/hole_in_fn.lean.expected.out
@@ -1,4 +1,4 @@
-hole_in_fn.lean:7:13: error: don't know how to synthesize placeholder
+hole_in_fn.lean:6:13: error: don't know how to synthesize placeholder
 state:
 n : ℕ
 ⊢ ℕ
diff --git a/tests/lean/hole_issue2.lean b/tests/lean/hole_issue2.lean
index 701d452e04..4902d45914 100644
--- a/tests/lean/hole_issue2.lean
+++ b/tests/lean/hole_issue2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 constant bag_setoid : ∀ A, setoid (list A)
 attribute [instance] bag_setoid
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index 8d08f27132..daf2d2fd96 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -1,4 +1,4 @@
-hole_issue2.lean:23:74: error: don't know how to synthesize placeholder
+hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
 state:
 A : Type,
 b₁ b₂ : bag A,
@@ -9,7 +9,7 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
 w : A,
 hw : ¬list.count w l₁ ≤ list.count w l₂
 ⊢ false
-hole_issue2.lean:30:65: error: don't know how to synthesize placeholder
+hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
 state:
 A : Type,
 b₁ b₂ : bag A,
@@ -18,7 +18,7 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
-hole_issue2.lean:37:28: error: don't know how to synthesize placeholder
+hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
 state:
 A : Type,
 b₁ b₂ : bag A,
diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean
index aed7ce1efc..f2f55e80a0 100644
--- a/tests/lean/inaccessible2.lean
+++ b/tests/lean/inaccessible2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive imf {A B : Type*} (f : A → B) : B → Type*
 | mk : ∀ (a : A), imf (f a)
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index e687a5fc1e..2bd649c553 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1,4 +1,4 @@
-inaccessible2.lean:7:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
-inaccessible2.lean:10:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
-inaccessible2.lean:13:13: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
-inaccessible2.lean:16:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
+inaccessible2.lean:6:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
+inaccessible2.lean:9:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+inaccessible2.lean:12:13: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+inaccessible2.lean:15:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 30dd97979e..d441e569ea 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true --
 set_option pp.notation false
 
 inductive [class] C (A : Type*)
diff --git a/tests/lean/instance_cache1.lean b/tests/lean/instance_cache1.lean
index bc1d6752f2..a01d651393 100644
--- a/tests/lean/instance_cache1.lean
+++ b/tests/lean/instance_cache1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f (A : Type*) (a : A) :=
 have has_add A, from has_add.mk (λ (a b : A), a),
diff --git a/tests/lean/instance_cache1.lean.expected.out b/tests/lean/instance_cache1.lean.expected.out
index 26248627e4..c7260ce768 100644
--- a/tests/lean/instance_cache1.lean.expected.out
+++ b/tests/lean/instance_cache1.lean.expected.out
@@ -1,14 +1,14 @@
-instance_cache1.lean:5:2: error: failed to synthesize type class instance for
+instance_cache1.lean:4:2: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 this : has_add A
 ⊢ has_add A
-instance_cache1.lean:8:7: error: failed to synthesize type class instance for
+instance_cache1.lean:7:7: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
 ⊢ has_add A
-instance_cache1.lean:11:19: error: failed to synthesize type class instance for
+instance_cache1.lean:10:19: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index fdd9fb0fdb..b762e81109 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -1,5 +1,4 @@
 prelude -- Correct version
-set_option new_elaborator true
 check let bool                      := Type.{0},
           and  (p q : bool)         := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25             := and,
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 99ced77ee5..6ef6674a43 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -6,7 +6,7 @@ let bool : Type := Prop,
     and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2)
 in and_intro :
   ∀ (p q : Prop), p → q → ∀ (c : Prop), (p → q → c) → c
-let1.lean:20:19: error: invalid let-expression, expression
+let1.lean:19:19: error: invalid let-expression, expression
   λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2
 has type
   Π (p q : bool), p → q → Π (c : bool), (p → q → c) → c
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index 8eb3d8a438..3a7890dbca 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,5 +1,4 @@
 --
-set_option new_elaborator true
 
 constant f : num → num → num → num
 
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index d613852b3c..893dc870df 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,5 +1,4 @@
 --
-set_option new_elaborator true
 
 constant f : num → num → num → num
 
diff --git a/tests/lean/non_exhaustive_error.lean b/tests/lean/non_exhaustive_error.lean
index 1025ce6f38..b95ed33a39 100644
--- a/tests/lean/non_exhaustive_error.lean
+++ b/tests/lean/non_exhaustive_error.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f : string → nat → bool
 | "hello world" 1 := tt
diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out
index 9d11afb8fd..56703eab52 100644
--- a/tests/lean/non_exhaustive_error.lean.expected.out
+++ b/tests/lean/non_exhaustive_error.lean.expected.out
@@ -1 +1 @@
-non_exhaustive_error.lean:3:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
+non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/print_ax3.lean b/tests/lean/print_ax3.lean
index eb8cadb164..d2032e09d1 100644
--- a/tests/lean/print_ax3.lean
+++ b/tests/lean/print_ax3.lean
@@ -1,4 +1,3 @@
-open subtype set_option new_elaborator true
 theorem foo1 : 0 = (0:num) :=
 rfl
 
diff --git a/tests/lean/red.lean b/tests/lean/red.lean
index bb2d83988c..bdf39fe493 100644
--- a/tests/lean/red.lean
+++ b/tests/lean/red.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 constant g : nat → nat
 
 noncomputable definition f := g
diff --git a/tests/lean/red.lean.expected.out b/tests/lean/red.lean.expected.out
index 953579bcb4..35fbda2da8 100644
--- a/tests/lean/red.lean.expected.out
+++ b/tests/lean/red.lean.expected.out
@@ -1,16 +1,16 @@
-red.lean:10:19: error: type mismatch, expression
+red.lean:9:19: error: type mismatch, expression
   rfl
 has type
   ?m_2 = ?m_2
 but is expected to have type
   f = g
-red.lean:13:0: error: "eliminator" elaborator type mismatch, term
+red.lean:12:0: error: "eliminator" elaborator type mismatch, term
   rfl
 has type
   ?m_2 = ?m_2
 but is expected to have type
   f a = a
-red.lean:18:0: error: "eliminator" elaborator type mismatch, term
+red.lean:17:0: error: "eliminator" elaborator type mismatch, term
   rfl
 has type
   ?m_2 = ?m_2
diff --git a/tests/lean/run/662.lean b/tests/lean/run/662.lean
index bee6cb345c..c6a8689765 100644
--- a/tests/lean/run/662.lean
+++ b/tests/lean/run/662.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 inductive type : Type
diff --git a/tests/lean/run/K_new_elab.lean b/tests/lean/run/K_new_elab.lean
index 3b1c9bcd66..a923b35daf 100644
--- a/tests/lean/run/K_new_elab.lean
+++ b/tests/lean/run/K_new_elab.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 theorem ex2 {A : Type} (H : A = A) (a : A) : cast H a = a :=
 rfl
diff --git a/tests/lean/run/assoc_flat.lean b/tests/lean/run/assoc_flat.lean
index 144333ee74..c10c5aa4c7 100644
--- a/tests/lean/run/assoc_flat.lean
+++ b/tests/lean/run/assoc_flat.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic expr
 
 constant nat.add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
diff --git a/tests/lean/run/at_at_bug.lean b/tests/lean/run/at_at_bug.lean
index 9fbca2852c..b9af3f9ea5 100644
--- a/tests/lean/run/at_at_bug.lean
+++ b/tests/lean/run/at_at_bug.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b :=
 @@eq.subst (λ x, p x b) h₂ h₁
diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean
index af7de24a80..d72bfaa70d 100644
--- a/tests/lean/run/basic.lean
+++ b/tests/lean/run/basic.lean
@@ -1,5 +1,4 @@
 prelude
-set_option new_elaborator true
 
 constant {l1 l2} A : Type l1 → Type l2
 check A
diff --git a/tests/lean/run/cases_bug3.lean b/tests/lean/run/cases_bug3.lean
index f4bfd428b5..f709594db0 100644
--- a/tests/lean/run/cases_bug3.lean
+++ b/tests/lean/run/cases_bug3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a'
 | a .a (heq.refl .a) := eq.refl a
diff --git a/tests/lean/run/cases_tac1.lean b/tests/lean/run/cases_tac1.lean
index cab542e081..acb0fe39ef 100644
--- a/tests/lean/run/cases_tac1.lean
+++ b/tests/lean/run/cases_tac1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type*) : nat → Type*
 | nil  : vec 0
diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean
index 6643877ceb..1b19094ae5 100644
--- a/tests/lean/run/choice_ctx.lean
+++ b/tests/lean/run/choice_ctx.lean
@@ -1,7 +1,6 @@
 open nat
 open eq
 set_option pp.coercions true
-set_option new_elaborator true
 namespace foo
 theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
 trans H1 H2
diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index 388d00e759..14f7ef36b4 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open prod inhabited
 
 definition H : inhabited (Prop × num × (num → num)) :=
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index 99296350f3..11c764d7b5 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
 := by apply_instance
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 4ad0816a92..ac7801fbdb 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 section
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index 5aa6c19851..1e1c9acd71 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 inductive t1 : Type
diff --git a/tests/lean/run/const_choice.lean b/tests/lean/run/const_choice.lean
index 129c5bb508..bcf1f3373a 100644
--- a/tests/lean/run/const_choice.lean
+++ b/tests/lean/run/const_choice.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition mypred (a : nat) : nat :=
diff --git a/tests/lean/run/contra3.lean b/tests/lean/run/contra3.lean
index ace48cfc27..393817e791 100644
--- a/tests/lean/run/contra3.lean
+++ b/tests/lean/run/contra3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic nat
 
 example (a b c : Prop) : a → b → ¬ a → c :=
diff --git a/tests/lean/run/dec_trivial_problem.lean b/tests/lean/run/dec_trivial_problem.lean
index 8b3773e0bd..f28d5fb498 100644
--- a/tests/lean/run/dec_trivial_problem.lean
+++ b/tests/lean/run/dec_trivial_problem.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition n : nat := 3
 
diff --git a/tests/lean/run/def1.lean b/tests/lean/run/def1.lean
index e94831ebd0..5f089f6c50 100644
--- a/tests/lean/run/def1.lean
+++ b/tests/lean/run/def1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 namespace tst
 variable {A : Type}
diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index 3e98929f48..86ff74ffff 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -5,7 +5,6 @@ inductive bv : nat → Type
 | cons : ∀ (n) (hd : bool) (tl : bv n), bv (succ n)
 
 open bv bool
-set_option new_elaborator true
 
 definition h : ∀ {n}, bv (succ (succ n)) → bool
 | .(succ m) (cons (succ (succ m)) b v) := b
diff --git a/tests/lean/run/def11.lean b/tests/lean/run/def11.lean
index 557f418fa5..b03d8c7047 100644
--- a/tests/lean/run/def11.lean
+++ b/tests/lean/run/def11.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition ex1 (a : nat) : nat.succ a = 0 → false
 .
diff --git a/tests/lean/run/def12.lean b/tests/lean/run/def12.lean
index f0eca4c585..4e94faab53 100644
--- a/tests/lean/run/def12.lean
+++ b/tests/lean/run/def12.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 theorem bit0_succ_eq (n : ℕ) : bit0 (succ n) = succ (succ (bit0 n)) :=
diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
index 5e5d423ed4..4901ecdee4 100644
--- a/tests/lean/run/def13.lean
+++ b/tests/lean/run/def13.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type) : nat → Type
 | nil {} : vec 0
diff --git a/tests/lean/run/def2.lean b/tests/lean/run/def2.lean
index 3a2293fa26..0037c4ec98 100644
--- a/tests/lean/run/def2.lean
+++ b/tests/lean/run/def2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition plus (a b : nat) : nat :=
 nat.rec_on a b (λ a' ih, nat.succ ih)
diff --git a/tests/lean/run/def3.lean b/tests/lean/run/def3.lean
index a31a3d74e6..8377bf1e52 100644
--- a/tests/lean/run/def3.lean
+++ b/tests/lean/run/def3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f (a b : nat) : nat :=
 nat.cases_on a
diff --git a/tests/lean/run/def4.lean b/tests/lean/run/def4.lean
index 51a3d0a7e9..d142185cea 100644
--- a/tests/lean/run/def4.lean
+++ b/tests/lean/run/def4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 section
   variable (A : Type)
diff --git a/tests/lean/run/def5.lean b/tests/lean/run/def5.lean
index c6d8127605..ef25c02b8a 100644
--- a/tests/lean/run/def5.lean
+++ b/tests/lean/run/def5.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 section
   parameter (A : Type)
diff --git a/tests/lean/run/def6.lean b/tests/lean/run/def6.lean
index 4fa79ee176..a5c0306891 100644
--- a/tests/lean/run/def6.lean
+++ b/tests/lean/run/def6.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type) : nat → Type
 | nil {} : vec 0
diff --git a/tests/lean/run/def7.lean b/tests/lean/run/def7.lean
index 4eb43b49df..ac30643a6f 100644
--- a/tests/lean/run/def7.lean
+++ b/tests/lean/run/def7.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f : bool → bool → nat
 | _ _ := 10
diff --git a/tests/lean/run/def8.lean b/tests/lean/run/def8.lean
index f257a13612..a2692880cc 100644
--- a/tests/lean/run/def8.lean
+++ b/tests/lean/run/def8.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive imf {A B : Type} (f : A → B) : B → Type
 | mk : ∀ (a : A), imf (f a)
diff --git a/tests/lean/run/def9.lean b/tests/lean/run/def9.lean
index 3855d02655..a05ac5068b 100644
--- a/tests/lean/run/def9.lean
+++ b/tests/lean/run/def9.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 lemma ex4 (A : Type) : ∀ (a b : A) (H : a = b), b = a
 | .z z (eq.refl .z) := eq.refl z
diff --git a/tests/lean/run/def_alias.lean b/tests/lean/run/def_alias.lean
index 43113f4944..516e4ff10d 100644
--- a/tests/lean/run/def_alias.lean
+++ b/tests/lean/run/def_alias.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 attribute [reducible]
 definition N := nat
diff --git a/tests/lean/run/def_brec1.lean b/tests/lean/run/def_brec1.lean
index 5f0accbfd1..470e1550c9 100644
--- a/tests/lean/run/def_brec1.lean
+++ b/tests/lean/run/def_brec1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive foo : bool → Type
 | Z  : foo ff
diff --git a/tests/lean/run/def_brec2.lean b/tests/lean/run/def_brec2.lean
index d20db96dc7..a2f67416e5 100644
--- a/tests/lean/run/def_brec2.lean
+++ b/tests/lean/run/def_brec2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option trace.eqn_compiler true
 
 definition fib : nat → nat
diff --git a/tests/lean/run/def_brec3.lean b/tests/lean/run/def_brec3.lean
index 2b430a8223..6a4b6d81b3 100644
--- a/tests/lean/run/def_brec3.lean
+++ b/tests/lean/run/def_brec3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 inductive bv : nat → Type
diff --git a/tests/lean/run/def_brec4.lean b/tests/lean/run/def_brec4.lean
index 213bd633bd..957891c413 100644
--- a/tests/lean/run/def_brec4.lean
+++ b/tests/lean/run/def_brec4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 inductive bv : nat → Type
diff --git a/tests/lean/run/def_brec_reflexive.lean b/tests/lean/run/def_brec_reflexive.lean
index 16bda5b8c1..bd6baa6eb4 100644
--- a/tests/lean/run/def_brec_reflexive.lean
+++ b/tests/lean/run/def_brec_reflexive.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive inftree (A : Type*)
 | leaf : A → inftree
diff --git a/tests/lean/run/def_complete_bug.lean b/tests/lean/run/def_complete_bug.lean
index 18d38dbbdc..7fe14e656a 100644
--- a/tests/lean/run/def_complete_bug.lean
+++ b/tests/lean/run/def_complete_bug.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition g : list nat → list nat → nat
 | []          (y::ys)  := y
diff --git a/tests/lean/run/def_ite1.lean b/tests/lean/run/def_ite1.lean
index d2f3638c36..e0f93c03bf 100644
--- a/tests/lean/run/def_ite1.lean
+++ b/tests/lean/run/def_ite1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f : nat → nat → nat
 | 100 2 := 0
diff --git a/tests/lean/run/def_ite_value.lean b/tests/lean/run/def_ite_value.lean
index 2815a36a97..6f12d2ef97 100644
--- a/tests/lean/run/def_ite_value.lean
+++ b/tests/lean/run/def_ite_value.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive bv : nat → Type
 | nil  : bv 0
diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean
index b4ec23bbad..1fc1c89705 100644
--- a/tests/lean/run/div_wf.lean
+++ b/tests/lean/run/div_wf.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat well_founded decidable prod
 
 set_option pp.all true
diff --git a/tests/lean/run/e4.lean b/tests/lean/run/e4.lean
index 255c8d4af1..b378203fe6 100644
--- a/tests/lean/run/e4.lean
+++ b/tests/lean/run/e4.lean
@@ -1,5 +1,4 @@
 prelude
-set_option new_elaborator true
 definition Prop := Type.{0}
 
 definition false : Prop := ∀x : Prop, x
diff --git a/tests/lean/run/elab_meta1.lean b/tests/lean/run/elab_meta1.lean
index eb7cf68d25..f63260d440 100644
--- a/tests/lean/run/elab_meta1.lean
+++ b/tests/lean/run/elab_meta1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 meta_definition f : nat → nat
 | n := if n / 2 = 0 then n + 1 else f (n / 2) + 1
diff --git a/tests/lean/run/empty_eq.lean b/tests/lean/run/empty_eq.lean
index 317716760c..d4a836f38d 100644
--- a/tests/lean/run/empty_eq.lean
+++ b/tests/lean/run/empty_eq.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 inductive Fin : nat → Type
diff --git a/tests/lean/run/empty_match.lean b/tests/lean/run/empty_match.lean
index 5d9a344270..23147a1c42 100644
--- a/tests/lean/run/empty_match.lean
+++ b/tests/lean/run/empty_match.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition not_lt_zero (a : nat) : ¬ a < 0 :=
diff --git a/tests/lean/run/empty_match_bug.lean b/tests/lean/run/empty_match_bug.lean
index 6e0a9ec12c..65f8d5d848 100644
--- a/tests/lean/run/empty_match_bug.lean
+++ b/tests/lean/run/empty_match_bug.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 inductive Fin : nat → Type
diff --git a/tests/lean/run/eq1.lean b/tests/lean/run/eq1.lean
index dbbeef544f..a238f7f10d 100644
--- a/tests/lean/run/eq1.lean
+++ b/tests/lean/run/eq1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 inductive day
 | monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
diff --git a/tests/lean/run/eq10.lean b/tests/lean/run/eq10.lean
index 9c2e67dee7..a55137b9fd 100644
--- a/tests/lean/run/eq10.lean
+++ b/tests/lean/run/eq10.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive formula
 | eqf  : nat → nat → formula
diff --git a/tests/lean/run/eq11.lean b/tests/lean/run/eq11.lean
index 6c691b91c0..185db76bc9 100644
--- a/tests/lean/run/eq11.lean
+++ b/tests/lean/run/eq11.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 inductive day
 | monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
diff --git a/tests/lean/run/eq12.lean b/tests/lean/run/eq12.lean
index 49ecb6ecd0..1c134fec69 100644
--- a/tests/lean/run/eq12.lean
+++ b/tests/lean/run/eq12.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat bool inhabited
 
 definition diag : bool → bool → bool → nat
diff --git a/tests/lean/run/eq13.lean b/tests/lean/run/eq13.lean
index 3b2364beb1..5fdba119f9 100644
--- a/tests/lean/run/eq13.lean
+++ b/tests/lean/run/eq13.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition f : nat → nat → nat
diff --git a/tests/lean/run/eq15.lean b/tests/lean/run/eq15.lean
index db92a2271c..de98b67232 100644
--- a/tests/lean/run/eq15.lean
+++ b/tests/lean/run/eq15.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open list
 
 set_option pp.implicit true
diff --git a/tests/lean/run/eq16.lean b/tests/lean/run/eq16.lean
index 7f323640ba..394b151f8e 100644
--- a/tests/lean/run/eq16.lean
+++ b/tests/lean/run/eq16.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open list
 
 variable {A : Type}
diff --git a/tests/lean/run/eq17.lean b/tests/lean/run/eq17.lean
index 7ef9153761..82aada223e 100644
--- a/tests/lean/run/eq17.lean
+++ b/tests/lean/run/eq17.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 attribute [pattern] lt.base
 attribute [pattern] lt.step
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index 55539eeee9..266c3424d3 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
 | a .a rfl := rfl
diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean
index 49245f5cbb..0649779aba 100644
--- a/tests/lean/run/eq20.lean
+++ b/tests/lean/run/eq20.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat list
 
 section
diff --git a/tests/lean/run/eq21.lean b/tests/lean/run/eq21.lean
index dad7aac850..141a9c3571 100644
--- a/tests/lean/run/eq21.lean
+++ b/tests/lean/run/eq21.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive formula
 | eqf  : nat → nat → formula
diff --git a/tests/lean/run/eq22.lean b/tests/lean/run/eq22.lean
index 090e022e93..1ea1a5daf3 100644
--- a/tests/lean/run/eq22.lean
+++ b/tests/lean/run/eq22.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open list
 
 definition head {A : Type} : Π (l : list A), l ≠ nil → A
diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean
index 9821198a29..ca08ec8aa0 100644
--- a/tests/lean/run/eq25.lean
+++ b/tests/lean/run/eq25.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 inductive N
 | O : N
 | S : N → N
diff --git a/tests/lean/run/eq4.lean b/tests/lean/run/eq4.lean
index 6590a43fb5..1298764aaa 100644
--- a/tests/lean/run/eq4.lean
+++ b/tests/lean/run/eq4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition half : nat → nat
diff --git a/tests/lean/run/eq5.lean b/tests/lean/run/eq5.lean
index ebe25c61cc..77f9f9a7a8 100644
--- a/tests/lean/run/eq5.lean
+++ b/tests/lean/run/eq5.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition fib : nat → nat
diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean
index 55ab38f9f1..66ac3d0838 100644
--- a/tests/lean/run/eq6.lean
+++ b/tests/lean/run/eq6.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open list
 
 definition appd {A : Type} : list A → list A → list A
diff --git a/tests/lean/run/eq9.lean b/tests/lean/run/eq9.lean
index 3a975a35ba..cf427791b4 100644
--- a/tests/lean/run/eq9.lean
+++ b/tests/lean/run/eq9.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 attribute [pattern] lt.base
 attribute [pattern] lt.step
diff --git a/tests/lean/run/exists_intro1.lean b/tests/lean/run/exists_intro1.lean
index 17b8a7f3d2..48cd5e8ce8 100644
--- a/tests/lean/run/exists_intro1.lean
+++ b/tests/lean/run/exists_intro1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 example : ∃ x : nat, x = x :=
 Exists.intro 0 rfl
diff --git a/tests/lean/run/fib_wrec.lean b/tests/lean/run/fib_wrec.lean
index dd5c6efe2d..c0e0eca5e0 100644
--- a/tests/lean/run/fib_wrec.lean
+++ b/tests/lean/run/fib_wrec.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition fib.F (n : nat) : (Π (m : nat), m < n → nat) → nat :=
diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean
index 09eaa68d9c..f896a36bc5 100644
--- a/tests/lean/run/interp.lean
+++ b/tests/lean/run/interp.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open bool nat
 open function
 
diff --git a/tests/lean/run/let1.lean b/tests/lean/run/let1.lean
index abef480117..3c7d3868e0 100644
--- a/tests/lean/run/let1.lean
+++ b/tests/lean/run/let1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 check
   let f x y := x ∧ y,
       g x   := f x x,
diff --git a/tests/lean/run/let2.lean b/tests/lean/run/let2.lean
index c0f8859281..e37b9f9b4b 100644
--- a/tests/lean/run/let2.lean
+++ b/tests/lean/run/let2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 definition b :=
       let a := true ∧ true,
           a := a ∧ a,
diff --git a/tests/lean/run/let3.lean b/tests/lean/run/let3.lean
index 36e2332311..1987d9cd50 100644
--- a/tests/lean/run/let3.lean
+++ b/tests/lean/run/let3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition p1 := (10, 20, 30)
 
diff --git a/tests/lean/run/lift_nested_rec.lean b/tests/lean/run/lift_nested_rec.lean
index ea2b61d6bf..7bdce4497d 100644
--- a/tests/lean/run/lift_nested_rec.lean
+++ b/tests/lean/run/lift_nested_rec.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition f : nat → (nat × nat) → nat
 | 0      m := m.1
diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean
index 7887c191b7..d07e0f0c96 100644
--- a/tests/lean/run/match3.lean
+++ b/tests/lean/run/match3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 definition foo (a : nat) : nat :=
diff --git a/tests/lean/run/match_anonymous_constructor.lean b/tests/lean/run/match_anonymous_constructor.lean
index a0ee4b9dbf..aa47991145 100644
--- a/tests/lean/run/match_anonymous_constructor.lean
+++ b/tests/lean/run/match_anonymous_constructor.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 definition p1 := (10, 20, 30)
 
diff --git a/tests/lean/run/match_convoy2.lean b/tests/lean/run/match_convoy2.lean
index e3efb45814..a3670a53ea 100644
--- a/tests/lean/run/match_convoy2.lean
+++ b/tests/lean/run/match_convoy2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type) : nat → Type
 | nil {} : vec nat.zero
diff --git a/tests/lean/run/match_convoy3.lean b/tests/lean/run/match_convoy3.lean
index fb446b1786..8d65aa7efc 100644
--- a/tests/lean/run/match_convoy3.lean
+++ b/tests/lean/run/match_convoy3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 constant bag_setoid : ∀ A, setoid (list A)
 attribute [instance] bag_setoid
diff --git a/tests/lean/run/match_fun.lean b/tests/lean/run/match_fun.lean
index 7209c30236..a31313099b 100644
--- a/tests/lean/run/match_fun.lean
+++ b/tests/lean/run/match_fun.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open bool nat
 
 definition foo (b : bool) : nat → nat :=
diff --git a/tests/lean/run/match_pattern2.lean b/tests/lean/run/match_pattern2.lean
index 614010d483..5a9391e14a 100644
--- a/tests/lean/run/match_pattern2.lean
+++ b/tests/lean/run/match_pattern2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic list expr
 
 private meta_definition pattern_telescope : expr → list expr → tactic (list expr × expr × expr)
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 4adb0e6463..1cd708e9ed 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -1,5 +1,4 @@
 import system.IO
-set_option new_elaborator true
 
 meta_definition foo : nat → nat
 | a := nat.cases_on a 1 (λ n, foo n + 2)
diff --git a/tests/lean/run/meta_tac1.lean b/tests/lean/run/meta_tac1.lean
index d62cfcee5b..2207e8f60f 100644
--- a/tests/lean/run/meta_tac1.lean
+++ b/tests/lean/run/meta_tac1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option pp.all true
 
 open tactic list
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index d0905e2a21..843d38984b 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open decidable open eq
 namespace experiment
 inductive nat : Type
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index eeba2409c5..335e675c50 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 namespace experiment
 inductive nat : Type
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index 9d4b3580ba..c0bcfb924c 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 namespace experiment
 inductive nat : Type
 | zero : nat
diff --git a/tests/lean/run/new_elab1.lean b/tests/lean/run/new_elab1.lean
index 656de537cc..8799fcd8ba 100644
--- a/tests/lean/run/new_elab1.lean
+++ b/tests/lean/run/new_elab1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 protected theorem my_add_comm : ∀ (n m : ℕ), n + m = m + n
diff --git a/tests/lean/run/new_elab2.lean b/tests/lean/run/new_elab2.lean
index c5f94b3671..fc6d040e57 100644
--- a/tests/lean/run/new_elab2.lean
+++ b/tests/lean/run/new_elab2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 theorem ex {a : Prop} (H : ¬a) : a ↔ false :=
 iff.intro H (false.rec a)
diff --git a/tests/lean/run/no_confusion1.lean b/tests/lean/run/no_confusion1.lean
index c2830079e5..190fd09082 100644
--- a/tests/lean/run/no_confusion1.lean
+++ b/tests/lean/run/no_confusion1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 theorem ex1 (n : nat) : bit0 n ≠ 1 :=
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index 398eaff4c3..d686ebc6f8 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/tests/lean/run/occurs_check_bug1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat prod
 open decidable
 
diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
index 1d5f2c33ca..f890b3557a 100644
--- a/tests/lean/run/over_subst.lean
+++ b/tests/lean/run/over_subst.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 namespace experiment
 namespace nat
 constant nat : Type.{1}
diff --git a/tests/lean/run/overload_issue.lean b/tests/lean/run/overload_issue.lean
index adbb71b48e..7f85502f8d 100644
--- a/tests/lean/run/overload_issue.lean
+++ b/tests/lean/run/overload_issue.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 example : true :=
diff --git a/tests/lean/run/pack_unpack1.lean b/tests/lean/run/pack_unpack1.lean
index 813645e5b3..01ab870370 100644
--- a/tests/lean/run/pack_unpack1.lean
+++ b/tests/lean/run/pack_unpack1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive tree_core (A : Type*) : bool → Type*
 | leaf'    : A → tree_core ff
diff --git a/tests/lean/run/pack_unpack2.lean b/tests/lean/run/pack_unpack2.lean
index 66c13dd864..8c34e49fb1 100644
--- a/tests/lean/run/pack_unpack2.lean
+++ b/tests/lean/run/pack_unpack2.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 --set_option trace.inductive_compiler.nested.define true
 inductive tree (A : Type*)
 | leaf : A -> tree
diff --git a/tests/lean/run/pack_unpack3.lean b/tests/lean/run/pack_unpack3.lean
index 377db776a6..6c00d1434d 100644
--- a/tests/lean/run/pack_unpack3.lean
+++ b/tests/lean/run/pack_unpack3.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 inductive vec (A : Type*) : nat -> Type*
 | vnil : vec 0
diff --git a/tests/lean/run/parent_struct_inst.lean b/tests/lean/run/parent_struct_inst.lean
index c81f12d426..cdaaff88d8 100644
--- a/tests/lean/run/parent_struct_inst.lean
+++ b/tests/lean/run/parent_struct_inst.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 structure [class] A := (n : ℕ)
diff --git a/tests/lean/run/section4.lean b/tests/lean/run/section4.lean
index 91e73b1366..5cb4da3b24 100644
--- a/tests/lean/run/section4.lean
+++ b/tests/lean/run/section4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 set_option pp.universes true
 set_option pp.implicit true
 
diff --git a/tests/lean/run/section_var_bug.lean b/tests/lean/run/section_var_bug.lean
index 90b103534c..acf8b85cc5 100644
--- a/tests/lean/run/section_var_bug.lean
+++ b/tests/lean/run/section_var_bug.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 section
 variable {A : Type}
diff --git a/tests/lean/run/set_attr1.lean b/tests/lean/run/set_attr1.lean
index c5857415b1..7360aa34a2 100644
--- a/tests/lean/run/set_attr1.lean
+++ b/tests/lean/run/set_attr1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 constant f : nat → nat
diff --git a/tests/lean/run/sigma_match.lean b/tests/lean/run/sigma_match.lean
index cb9aace7ba..31f85efb8c 100644
--- a/tests/lean/run/sigma_match.lean
+++ b/tests/lean/run/sigma_match.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open sigma
 
 constant {l₁ l₂} hom {A : Type l₁} {B : Type l₂} (a : A) (b : B) : Type (max l₁ l₂)
diff --git a/tests/lean/run/simplifier_canonize_instances.lean b/tests/lean/run/simplifier_canonize_instances.lean
index e95a600aef..b92438b330 100644
--- a/tests/lean/run/simplifier_canonize_instances.lean
+++ b/tests/lean/run/simplifier_canonize_instances.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 set_option simplify.theory false
diff --git a/tests/lean/run/simplifier_canonize_subsingletons.lean b/tests/lean/run/simplifier_canonize_subsingletons.lean
index a064ed34ad..10f9ba80db 100644
--- a/tests/lean/run/simplifier_canonize_subsingletons.lean
+++ b/tests/lean/run/simplifier_canonize_subsingletons.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 namespace synth_congr
diff --git a/tests/lean/run/stateT1.lean b/tests/lean/run/stateT1.lean
index 501be6c896..f33b046f6c 100644
--- a/tests/lean/run/stateT1.lean
+++ b/tests/lean/run/stateT1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 meta_definition mytactic (A : Type) := stateT (list nat) tactic A
 
diff --git a/tests/lean/run/sufficies.lean b/tests/lean/run/sufficies.lean
index f79c882a16..0dcff7247b 100644
--- a/tests/lean/run/sufficies.lean
+++ b/tests/lean/run/sufficies.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 protected theorem one_le_bit0 (n : ℕ) : n ≠ 0 → 1 ≤ bit0 n :=
diff --git a/tests/lean/run/t4.lean b/tests/lean/run/t4.lean
index c96e7c1f89..4723a37fcd 100644
--- a/tests/lean/run/t4.lean
+++ b/tests/lean/run/t4.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 namespace foo
   definition {u} f (A : Type u) : Type u := A
   check f.{1}
diff --git a/tests/lean/run/t6.lean b/tests/lean/run/t6.lean
index cad90b6c66..07dc09eed6 100644
--- a/tests/lean/run/t6.lean
+++ b/tests/lean/run/t6.lean
@@ -1,5 +1,4 @@
 prelude
-set_option new_elaborator true
 precedence `+`  : 65
 precedence `++` : 100
 constant N : Type.{1}
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
old mode 100755
new mode 100644
index ec23fa82c5..0cce45ba64
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -8,7 +8,7 @@ LEAN=$1
 export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
-if "$LEAN" -Dnew_elaborator=true "$f"; then
+if "$LEAN" "$f"; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lean/run/unfold_crash.lean b/tests/lean/run/unfold_crash.lean
index 2036c76cc7..e70113e22c 100644
--- a/tests/lean/run/unfold_crash.lean
+++ b/tests/lean/run/unfold_crash.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 -- TODO(Leo): remove the following command.
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index f5882c078d..d56d97fb03 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 namespace experiment
 inductive nat : Type
 | zero : nat
diff --git a/tests/lean/run/whnfinst.lean b/tests/lean/run/whnfinst.lean
index a702af5e6b..a0d119f707 100644
--- a/tests/lean/run/whnfinst.lean
+++ b/tests/lean/run/whnfinst.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open decidable
 
 attribute [reducible]
diff --git a/tests/lean/sec_param_pp.lean b/tests/lean/sec_param_pp.lean
index 736c50171a..6e6b75f822 100644
--- a/tests/lean/sec_param_pp.lean
+++ b/tests/lean/sec_param_pp.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 section
  parameters {A : Type*} (a : A)
  variable f : A → A → A
diff --git a/tests/lean/set_attr1.lean b/tests/lean/set_attr1.lean
index 5cc9778fb5..0b4e2b7fc8 100644
--- a/tests/lean/set_attr1.lean
+++ b/tests/lean/set_attr1.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open tactic
 
 constant f : nat → nat
diff --git a/tests/lean/set_attr1.lean.expected.out b/tests/lean/set_attr1.lean.expected.out
index 19f05964eb..0cccbb6d30 100644
--- a/tests/lean/set_attr1.lean.expected.out
+++ b/tests/lean/set_attr1.lean.expected.out
@@ -1,4 +1,4 @@
-set_attr1.lean:15:0: error: tactic failed, result contains meta-variables
+set_attr1.lean:14:0: error: tactic failed, result contains meta-variables
 state:
 n : ℕ
 ⊢ f n = n + 1
diff --git a/tests/lean/synth_inferred_mismatch.lean b/tests/lean/synth_inferred_mismatch.lean
index 3e8d970231..91e8383404 100644
--- a/tests/lean/synth_inferred_mismatch.lean
+++ b/tests/lean/synth_inferred_mismatch.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 
 constant f   (c : Prop) [decidable c] : Prop
 constant fax (c : Prop) [decidable c] : f c
diff --git a/tests/lean/synth_inferred_mismatch.lean.expected.out b/tests/lean/synth_inferred_mismatch.lean.expected.out
index a85a9db497..9c2d321d86 100644
--- a/tests/lean/synth_inferred_mismatch.lean.expected.out
+++ b/tests/lean/synth_inferred_mismatch.lean.expected.out
@@ -1,4 +1,4 @@
-synth_inferred_mismatch.lean:8:1: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
+synth_inferred_mismatch.lean:7:1: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
   _inst_1
 inferred
   is_true h
diff --git a/tests/lean/tuple.lean b/tests/lean/tuple.lean
index 527e37a3df..8bd35a027b 100644
--- a/tests/lean/tuple.lean
+++ b/tests/lean/tuple.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true --
 open nat prod
 
 set_option pp.universes true
diff --git a/tests/lean/user_attribute.lean b/tests/lean/user_attribute.lean
index 986e91522b..27506fc8d5 100644
--- a/tests/lean/user_attribute.lean
+++ b/tests/lean/user_attribute.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 definition foo_attr : user_attribute := ⟨`foo, "bar"⟩
 run_command attribute.register `foo_attr
 
diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out
index d9b020ad29..52a84c3516 100644
--- a/tests/lean/user_attribute.lean.expected.out
+++ b/tests/lean/user_attribute.lean.expected.out
@@ -7,12 +7,12 @@ eq.refl
 attribute [foo, foo.baz, refl]
 constructor eq.refl : ∀ {A : Type u} (a : A), a = a
 [eq.refl]
-user_attribute.lean:25:0: error: an attribute named [reducible] has already been registered
+user_attribute.lean:24:0: error: an attribute named [reducible] has already been registered
 state:
 ⊢ true
-user_attribute.lean:30:0: error: invalid attribute.register argument, must be name of a definition of type user_attribute
+user_attribute.lean:29:0: error: invalid attribute.register argument, must be name of a definition of type user_attribute
 state:
 ⊢ true
-user_attribute.lean:36:2: error: invalid attribute.register argument, must be name of a definition of type user_attribute
+user_attribute.lean:35:2: error: invalid attribute.register argument, must be name of a definition of type user_attribute
 state:
 ⊢ true
diff --git a/tests/lean/wrong_arity.lean b/tests/lean/wrong_arity.lean
index deb4aa8e4f..aab37aa129 100644
--- a/tests/lean/wrong_arity.lean
+++ b/tests/lean/wrong_arity.lean
@@ -1,4 +1,3 @@
-set_option new_elaborator true
 open nat
 
 theorem succ_ne_self : ∀ (n : ℕ), succ n ≠ n
diff --git a/tests/lean/wrong_arity.lean.expected.out b/tests/lean/wrong_arity.lean.expected.out
index 93715733ad..806d096fd3 100644
--- a/tests/lean/wrong_arity.lean.expected.out
+++ b/tests/lean/wrong_arity.lean.expected.out
@@ -1 +1 @@
-wrong_arity.lean:6:6: error: invalid match/equations expression, each case must have the same number of patterns
+wrong_arity.lean:5:6: error: invalid match/equations expression, each case must have the same number of patterns