diff --git a/tests/lean/bad_error2.lean b/tests/lean/bad_error2.lean
index a05d56e7d1..f0f6afa860 100644
--- a/tests/lean/bad_error2.lean
+++ b/tests/lean/bad_error2.lean
@@ -4,7 +4,8 @@ example {k n m : ℕ} (h : k + n ≤ k + m) : n ≤ m :=
 match le.dest h with
 | ⟨w, hw⟩ := @le.intro _ _ w
     begin
-      -- in the following error pp.beta is automatically disabled
+      -- hw is beta reduced after we added the equation compiler preprocessor.
+      -- So, this test is not really relevant anymore.
       rw [nat.add_assoc] at hw,
       apply nat.add_left_cancel hw
     end
diff --git a/tests/lean/bad_error2.lean.expected.out b/tests/lean/bad_error2.lean.expected.out
index 838f3039fa..e69de29bb2 100644
--- a/tests/lean/bad_error2.lean.expected.out
+++ b/tests/lean/bad_error2.lean.expected.out
@@ -1,9 +0,0 @@
-bad_error2.lean:8:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
-  ?m_1 + ?m_2 + ?m_3
-state:
-k n m : ℕ,
-h : k + n ≤ k + m,
-_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
-w : ℕ,
-hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
-⊢ n + w = m
diff --git a/tests/lean/bad_inaccessible.lean b/tests/lean/bad_inaccessible.lean
index eabde01acb..0450738da8 100644
--- a/tests/lean/bad_inaccessible.lean
+++ b/tests/lean/bad_inaccessible.lean
@@ -1,3 +1,4 @@
+-- These definitions can be processed by the new equation compiler without producing errors.
 universe variables u
 definition f1 : 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 67a4610e88..e69de29bb2 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,7 +0,0 @@
-bad_inaccessible.lean:3:6: error: invalid use of inaccessible term, it is not fixed by other arguments
-bad_inaccessible.lean:6:8: error: invalid use of inaccessible term, the provided term is
-  b
-but is expected to be
-  a
-bad_inaccessible.lean:14:2: 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 ec97190b70..f4147a47ba 100644
--- a/tests/lean/bad_inaccessible2.lean
+++ b/tests/lean/bad_inaccessible2.lean
@@ -8,24 +8,14 @@ open vec
 variables {A : Type u}
 variables f : A → A → A
 
-/- The following definition fails because the pattern variables are
-   introduced in the following order:
-         a va n b vb
-   However, the type of va must be (vec A n). That is, it depends
-   on a variable introduced after va.
-
-   The error message is confusing.
-
-   Alternatives:
-   1- Ignore the problem since this is a very obscure use of inaccessible terms.
-   2- Reorder variables based on their occurrence in inaccessible terms.
-      If we do that, the variables in the pattern will be ordered as:
-            n a va b vb
-      and this example will work. This is not fully satisfactor since
-      we can create another declaration where this heuristic is not the right
-      solution.
-   3- Produce a better error message.
+/- The new equation compiler can process this example.
+   So, this is not a test about error messages anymore.
 -/
-definition map_head : ∀ {n}, vec A n → vec A n → vec A n
+def map_head : ∀ {n}, vec A n → vec A n → vec A n
 | .(0)     nil nil                       := nil
 | .(n+1) (@cons .(A) .(n) a va) (@cons .(A) n b vb) := cons (f a b) va
+
+/- The following shorter version is also accepted. -/
+def map_head2 : ∀ {n}, vec A n → vec A n → vec A n
+| _ nil         nil         := nil
+| _ (cons a va) (cons b vb) := cons (f a b) va
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index 181fc9d1a6..e69de29bb2 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -1,9 +0,0 @@
-bad_inaccessible2.lean:31:2: error: type mismatch at application
-  map_head (cons a va) (cons b vb)
-term
-  cons b vb
-has type
-  vec .?m_1 (n + 1)
-but is expected to have type
-  vec A . (.?m_1 + 1)
-bad_inaccessible2.lean:31:52: error: ill-formed match/equations expression
diff --git a/tests/lean/bad_pattern2.lean.expected.out b/tests/lean/bad_pattern2.lean.expected.out
index c3e86a06bb..3457b87bff 100644
--- a/tests/lean/bad_pattern2.lean.expected.out
+++ b/tests/lean/bad_pattern2.lean.expected.out
@@ -8,4 +8,4 @@ has type
   _
 but is expected to have type
   ℕ
-bad_pattern2.lean:2:10: error: ill-formed match/equations expression
+bad_pattern2.lean:2:10: error: ill-formed match/equation expression
diff --git a/tests/lean/def_inaccessible_issue.lean.expected.out b/tests/lean/def_inaccessible_issue.lean.expected.out
index 5599ccc6b4..023f20bc55 100644
--- a/tests/lean/def_inaccessible_issue.lean.expected.out
+++ b/tests/lean/def_inaccessible_issue.lean.expected.out
@@ -1,3 +1,3 @@
 map2.equations._eqn_2 :
-  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
-    map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)
+  ∀ (f : bool → bool → bool) (x : ℕ) (b1 : bool) (v1 : bv x) (b2 : bool) (v2 : bv x),
+    map2 f (cons x b1 v1) (cons x b2 v2) = cons x (f b1 b2) (map2 f v1 v2)
diff --git a/tests/lean/eqn_compiler_error_msg.lean.expected.out b/tests/lean/eqn_compiler_error_msg.lean.expected.out
index febe75ee50..a6cc4fdedc 100644
--- a/tests/lean/eqn_compiler_error_msg.lean.expected.out
+++ b/tests/lean/eqn_compiler_error_msg.lean.expected.out
@@ -1,3 +1,3 @@
-eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
-  .p + .n
+eqn_compiler_error_msg.lean:5:28: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
+  .?m_1 + .?m_2
 eqn_compiler_error_msg.lean:4:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/expr_quote.lean.expected.out b/tests/lean/expr_quote.lean.expected.out
index c5ecb9ea14..dd0b640062 100644
--- a/tests/lean/expr_quote.lean.expected.out
+++ b/tests/lean/expr_quote.lean.expected.out
@@ -1,4 +1,5 @@
 expr_quote.lean:1:30: error: invalid quotation, contains universe metavariable
+expr_quote.lean:1:9: error: type of sorry macro is not a sort
 expr_quote.lean:1:9: error: don't know how to synthesize placeholder
 context:
 α a : expr
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index 9094778491..d3b9902182 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -1,21 +1,24 @@
-inaccessible.lean:14:10: error: function expected at
-  mk
-term has type
-  ?m_1
-inaccessible.lean:14:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible.lean:14:10: error: invalid application, function expected
+inaccessible.lean:14:13: error: don't know how to synthesize placeholder
+context:
+A : Type u,
+B : Type v,
+f : A → B,
+inv_3 : Π (b : B), imf f b → A
+⊢ A
+inaccessible.lean:13:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
-inaccessible.lean:17:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible.lean:17:16: error: don't know how to synthesize placeholder
+context:
+A : Type u,
+B : Type v,
+f : A → B,
+inv_4 : Π (b : B), imf f b → A
+⊢ A
+inaccessible.lean:16:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
-inaccessible.lean:25:3: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible.lean:25:16: error: ill-formed match/equations expression
-inaccessible.lean:28:3: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible.lean:28:16: error: ill-formed match/equations expression
+inaccessible.lean:25:3: error: invalid application, function expected
+inaccessible.lean:25:16: error: ill-formed match/equation expression
+inaccessible.lean:28:3: error: invalid application, function expected
+inaccessible.lean:28:16: error: ill-formed match/equation expression
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
-inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
-  .?m_1 + 1
diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean
index eabd5f401f..6cf946e1f1 100644
--- a/tests/lean/inaccessible2.lean
+++ b/tests/lean/inaccessible2.lean
@@ -12,3 +12,6 @@ definition inv_3 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
 
 definition symm {A : Sort*} : ∀ a b : A, a = b → b = a
 | .(a) .(a) (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
+
+definition symm2 {A : Sort*} : ∀ a b : A, a = b → b = a
+| _ _ rfl := rfl -- correct version
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 84de31e298..0756178ca1 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1,14 +1,24 @@
 inaccessible2.lean:5:8: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:8:45: error: unknown identifier 'a'
-inaccessible2.lean:8:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible2.lean:7:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be used in patterns
 inaccessible2.lean:11:46: error: invalid expression
-inaccessible2.lean:11:4: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible2.lean:11:46: error: ill-formed match/equations expression
+inaccessible2.lean:11:4: error: invalid application, function expected
+inaccessible2.lean:11:46: error: ill-formed match/equation expression
 inaccessible2.lean:11:46: error: command expected
-inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
-inaccessible2.lean:14:24: error: ill-formed match/equations expression
+inaccessible2.lean:14:27: error: don't know how to synthesize placeholder
+context:
+A : Sort ?,
+symm : ∀ (a b : A), a = b → b = a
+⊢ A
+inaccessible2.lean:13:11: error: equation compiler failed to create auxiliary declaration 'symm._main'
+nested exception message:
+type mismatch at application
+  eq.rec (λ (a_1 : a = a) (H_2 : a_1 == eq.refl a), id_rhs (⁇ = ⁇) rfl)
+term
+  λ (a_1 : a = a) (H_2 : a_1 == eq.refl a), id_rhs (⁇ = ⁇) rfl
+has type
+  ∀ (a_1 : a = a), a_1 == _ → ⁇ = ⁇
+but is expected to have type
+  (λ (b : A), ∀ (a_1 : a = b), a_1 == _ → b = a) a
diff --git a/tests/lean/inject.lean.expected.out b/tests/lean/inject.lean.expected.out
index 0972e3501c..004e5cb2ff 100644
--- a/tests/lean/inject.lean.expected.out
+++ b/tests/lean/inject.lean.expected.out
@@ -3,12 +3,12 @@ lift.equations._eqn_2 : ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ), @lift m k
 lift.equations._eqn_3 :
   ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ) (i : fi (m + n)),
     @lift m k f (succ n) (@fs (m + n) i) = @fs (k + n) (@lift m k f n i)
-to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
-to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)
-inject.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
+to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
+to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)
+inject.equations._eqn_1 : ∀ (x : ℕ) (i : fi x), @inject (succ x) (@fs x i) (@f0 (@to_nat x i)) = @f0 x
 inject.equations._eqn_2 :
-  ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
-    @inject (succ n) (@fs n i) (@fs (@to_nat n i) j) = @fs n (@inject n i j)
+  ∀ (x : ℕ) (i : fi x) (j : fi (@to_nat x i)),
+    @inject (succ x) (@fs x i) (@fs (@to_nat x i) j) = @fs x (@inject x i j)
 inject'.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject' (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
 inject'.equations._eqn_2 :
   ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
@@ -16,10 +16,10 @@ inject'.equations._eqn_2 :
 raise.equations._eqn_1 : ∀ {m : ℕ} (i : fi m), @raise m 0 i = i
 raise.equations._eqn_2 : ∀ {m : ℕ} (n : ℕ) (i : fi m), @raise m (succ n) i = @fs (m + n) (@raise m n i)
 deg.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
+deg.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
 deg.equations._eqn_3 :
-  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg n i j)
+  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg x i j)
 deg'.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg' (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg'.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg' (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
+deg'.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg' (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
 deg'.equations._eqn_3 :
-  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg' (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg' n i j)
+  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg' (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg' x i j)
diff --git a/tests/lean/offset_is_def_eq_trick.lean.expected.out b/tests/lean/offset_is_def_eq_trick.lean.expected.out
index dda1efbaa4..56296405a7 100644
--- a/tests/lean/offset_is_def_eq_trick.lean.expected.out
+++ b/tests/lean/offset_is_def_eq_trick.lean.expected.out
@@ -1 +1 @@
-head.equations._eqn_1 : ∀ {α : Type u_1} (n : ℕ) (h : α) (t : Vec α n), head (Vec.cons h t) = h
+head.equations._eqn_1 : ∀ {α : Type u_1} (x : ℕ) (h : α) (t : Vec α x), head (Vec.cons h t) = h
diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out
index e0ce2e679e..90c86b64ea 100644
--- a/tests/lean/string_imp.lean.expected.out
+++ b/tests/lean/string_imp.lean.expected.out
@@ -1,10 +1,18 @@
 string_imp.lean:2:2: error: invalid constructor ⟨...⟩, type is a private inductive datatype
+string_imp.lean:2:3: error: don't know how to synthesize placeholder
+context:
+f : string → list char
+⊢ list char
 string_imp.lean:1:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 string_imp.lean:5:3: error: invalid pattern: variable, constructor or constant tagged as pattern expected
 string_imp.lean:5:3: error: function expected at
   string_imp.mk
 term has type
   _
+string_imp.lean:5:17: error: don't know how to synthesize placeholder
+context:
+g : string → list char
+⊢ list char
 string_imp.lean:4:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 string_imp.lean:8:0: error: unknown identifier 'string_imp.cases_on'
 string_imp.lean:7:0: warning: declaration 'h' uses sorry