fix: fix coercion of Heyting.Regular (#7293)

fpvandoorn · fpvandoorn · commit a526f3ebfd15 · 2023-09-21T13:09:08.000Z
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/import.20Mathlib.20leads.20to.20Lean.20not.20terminating)
diff --git a/Mathlib/Order/Heyting/Regular.lean b/Mathlib/Order/Heyting/Regular.lean
@@ -116,7 +116,7 @@ namespace Regular
 
 theorem prop : ∀ a : Regular α, IsRegular a.val := Subtype.prop
 
-instance : Coe (Regular α) α := ⟨Regular.val⟩
+instance : CoeOut (Regular α) α := ⟨Regular.val⟩
 
 theorem coe_injective : Injective ((↑) : Regular α → α) :=
   Subtype.coe_injective
