From cbd36e897b89ea6147437f73f28e2c3d3cd19df2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Aug 2021 06:16:46 -0700
Subject: [PATCH] chore: remove `ToExpr Expr`

---
 src/Lean/ToExpr.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 0f56dc29d4..a596974b2f 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -14,10 +14,6 @@ class ToExpr (α : Type u) where
 
 export ToExpr (toExpr toTypeExpr)
 
-instance : ToExpr Expr where
-  toExpr     := id
-  toTypeExpr := mkConst ``Expr
-
 instance : ToExpr Nat where
   toExpr     := mkNatLit
   toTypeExpr := mkConst ``Nat