From aedd59258bae5602bd625f0944f822c63fccaa97 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jan 2020 16:52:12 -0800
Subject: [PATCH] fix: missing file

---
 src/Init/Lean/Elab/Tactic.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 src/Init/Lean/Elab/Tactic.lean

diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
new file mode 100644
index 0000000000..c38a7d243f
--- /dev/null
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Elab.Term
+
+namespace Lean
+namespace Elab
+namespace Term
+
+@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
+fun stx _ =>
+  throwError stx ("not implemented yet " ++ stx)
+
+end Term
+
+end Elab
+end Lean