From 4d2efd4d086f779622fd8a69633f7a9cfd8686d1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Sep 2020 10:47:13 +0200
Subject: [PATCH] fix: HasOrelse (DelabM _)

---
 src/Lean/Delaborator.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 382c77b781..ca3ef57210 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -95,6 +95,8 @@ protected def failure {α} : DelabM α := throw $ Exception.internal delabFailur
 instance : Alternative DelabM :=
 { orelse  := fun _ => Delaborator.orelse,
   failure := fun _ => Delaborator.failure }
+-- HACK: necessary since it would otherwise prefer the instance from MonadExcept
+instance {α} : HasOrelse (DelabM α) := alternativeHasOrelse _ _
 
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.