From ba7d3ee178f3efac5cdd90fc7a3bb3994f7e3a60 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 6 Aug 2018 15:05:41 -0700
Subject: [PATCH] refactor(library/init/lean/parser/{reader/module,syntax}):
 move new coercions

---
 library/init/lean/parser/reader/module.lean | 6 ------
 library/init/lean/parser/syntax.lean        | 6 ++++++
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean
index 0160a6beff..1a88e2e3b9 100644
--- a/library/init/lean/parser/reader/module.lean
+++ b/library/init/lean/parser/reader/module.lean
@@ -269,12 +269,6 @@ end reader
 namespace reader
 open macro.has_view combinators
 
-instance string_syntax_coe : has_coe string syntax :=
-⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩
-
-instance name_syntax_coe : has_coe name syntax :=
-⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩
-
 def mixfix.expand (stx : syntax) : option syntax :=
 do v ← view mixfix stx,
    syntax.atom ⟨_, atomic_val.string kind⟩ ← pure v.kind | failure,
diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
index 5cbda6866e..88ece48389 100644
--- a/library/init/lean/parser/syntax.lean
+++ b/library/init/lean/parser/syntax.lean
@@ -55,6 +55,12 @@ inductive syntax
 instance : inhabited syntax :=
 ⟨syntax.missing⟩
 
+instance coe_string_syntax : has_coe string syntax :=
+⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩
+
+instance coe_name_syntax : has_coe name syntax :=
+⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩
+
 def substring.to_string (s : substring) : string :=
 (s.start.extract s.stop).get_or_else ""