From ef105ba49d811f658cc5b418fa3a701759df47bf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jan 2020 08:49:02 -0800
Subject: [PATCH] chore: remove `coe` functions

They will be used in the new `Coe` file
---
 src/Init/Coe.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 5ecf9f7cba..d390a1eeda 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -73,15 +73,6 @@ HasCoeToFun.coe
 @[reducible, inline] def oldCoeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
 HasCoeToSort.coe
 
-@[reducible, inline] def coe {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
-liftT
-
-@[reducible, inline] def coeFn {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
-HasCoeToFun.coe
-
-@[reducible, inline] def coeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
-HasCoeToSort.coe
-
 /- Notation -/
 
 universes u₁ u₂ u₃