From c8a42524615a463575ddfc59ef9f6e9fc89a9d43 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Sep 2020 16:53:53 -0700
Subject: [PATCH] refactor: move `OpenDecl` to `Data`

---
 src/Lean/Data/OpenDecl.lean    | 29 +++++++++++++++++++++++++++++
 src/Lean/Elab/ResolveName.lean | 20 +-------------------
 2 files changed, 30 insertions(+), 19 deletions(-)
 create mode 100644 src/Lean/Data/OpenDecl.lean

diff --git a/src/Lean/Data/OpenDecl.lean b/src/Lean/Data/OpenDecl.lean
new file mode 100644
index 0000000000..30e2f79c24
--- /dev/null
+++ b/src/Lean/Data/OpenDecl.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Data.Name
+
+namespace Lean
+
+inductive OpenDecl
+| simple   (ns : Name) (except : List Name)
+| explicit (id : Name) (declName : Name)
+
+namespace OpenDecl
+instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩
+
+instance : HasToString OpenDecl :=
+⟨fun decl => match decl with
+ | explicit id decl => toString id ++ " → " ++ toString decl
+ | simple ns ex     => toString ns ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩
+
+end OpenDecl
+
+def rootNamespace := `_root_
+
+def removeRoot (n : Name) : Name :=
+n.replacePrefix rootNamespace Name.anonymous
+
+end Lean
diff --git a/src/Lean/Elab/ResolveName.lean b/src/Lean/Elab/ResolveName.lean
index b7d03feb70..582382b605 100644
--- a/src/Lean/Elab/ResolveName.lean
+++ b/src/Lean/Elab/ResolveName.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
+import Lean.Data.OpenDecl
 import Lean.Hygiene
 import Lean.Modifiers
 import Lean.Elab.Alias
@@ -10,25 +11,6 @@ import Lean.Elab.Alias
 namespace Lean
 namespace Elab
 
-inductive OpenDecl
-| simple   (ns : Name) (except : List Name)
-| explicit (id : Name) (declName : Name)
-
-namespace OpenDecl
-instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩
-
-instance : HasToString OpenDecl :=
-⟨fun decl => match decl with
- | explicit id decl => toString id ++ " → " ++ toString decl
- | simple ns ex     => toString ns ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩
-
-end OpenDecl
-
-def rootNamespace := `_root_
-
-def removeRoot (n : Name) : Name :=
-n.replacePrefix rootNamespace Name.anonymous
-
 /- Global name resolution -/
 
 /- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/