From 8a48a8f119653ff0156d41e69bdf807a3641abc1 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 21 Dec 2022 11:50:04 -0800
Subject: [PATCH] refactor: use coercion meta API

---
 src/Lean/Elab/Extra.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 854b418a29..3d4851f536 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -197,11 +197,9 @@ where
 
 -- Auxiliary function used at `analyze`
 private def hasCoe (fromType toType : Expr) : TermElabM Bool := do
-  if (← getEnv).contains ``CoeHTCT then
-    let u ← getLevel fromType
-    let v ← getLevel toType
-    let coeInstType := mkAppN (Lean.mkConst ``CoeHTCT [u, v]) #[fromType, toType]
-    match ← trySynthInstance coeInstType (some (maxCoeSize.get (← getOptions))) with
+  if (← getEnv).contains ``CoeT then
+    withLocalDeclD `x fromType fun x => do
+    match ← coerceSimple? x toType with
     | .some _ => return true
     | .none   => return false
     | .undef  => return false -- TODO: should we do something smarter here?