From 5d6bf38b7e10950799ebb44261d030509b6e15b4 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 23 May 2017 07:33:12 +0200
Subject: [PATCH] chore(tests): add Leo's test case for errors in solve1-blocks

---
 tests/lean/auto_quote_error2.lean              | 8 ++++++++
 tests/lean/auto_quote_error2.lean.expected.out | 5 +++++
 2 files changed, 13 insertions(+)

diff --git a/tests/lean/auto_quote_error2.lean b/tests/lean/auto_quote_error2.lean
index 1e9cd714ea..47f2832654 100644
--- a/tests/lean/auto_quote_error2.lean
+++ b/tests/lean/auto_quote_error2.lean
@@ -45,3 +45,11 @@ begin
    { subst h1 },
             --^ error should be at `}`
 end
+
+example : true :=
+begin
+  {
+    note h' := eq.refl _,
+            --^  error should be on this line
+   }
+end
\ No newline at end of file
diff --git a/tests/lean/auto_quote_error2.lean.expected.out b/tests/lean/auto_quote_error2.lean.expected.out
index 153140b3f5..64fce7670a 100644
--- a/tests/lean/auto_quote_error2.lean.expected.out
+++ b/tests/lean/auto_quote_error2.lean.expected.out
@@ -42,3 +42,8 @@ state:
 b : ℕ,
 h2 : b = 0
 ⊢ 0 = b
+auto_quote_error2.lean:52:15: error: don't know how to synthesize placeholder
+context:
+⊢ Sort ?
+state:
+⊢ true