From 4b03666eccad726d459cdb9dd6034f0089f60aaa Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Feb 2022 09:28:24 +0100
Subject: [PATCH] chore: include orphan file

---
 src/Lean/Meta/Tactic.lean             | 1 +
 src/Lean/Meta/Tactic/LinearArith.lean | 6 ++++++
 2 files changed, 7 insertions(+)
 create mode 100644 src/Lean/Meta/Tactic/LinearArith.lean

diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean
index c09dac9406..18b2fefedf 100644
--- a/src/Lean/Meta/Tactic.lean
+++ b/src/Lean/Meta/Tactic.lean
@@ -25,3 +25,4 @@ import Lean.Meta.Tactic.Split
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Tactic.Rename
+import Lean.Meta.Tactic.LinearArith
diff --git a/src/Lean/Meta/Tactic/LinearArith.lean b/src/Lean/Meta/Tactic/LinearArith.lean
new file mode 100644
index 0000000000..ed683ee4aa
--- /dev/null
+++ b/src/Lean/Meta/Tactic/LinearArith.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+import Lean.Meta.Tactic.LinearArith.Basic