From 0334bcb1bfdb5735fec6e3ed5a0f404ed4a48698 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 16 Dec 2020 10:53:27 -0800
Subject: [PATCH] chore: update stage0

---
 stage0/src/Init/Classical.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stage0/src/Init/Classical.lean b/stage0/src/Init/Classical.lean
index 720e3ce4c6..8efcfc1760 100644
--- a/stage0/src/Init/Classical.lean
+++ b/stage0/src/Init/Classical.lean
@@ -68,7 +68,7 @@ noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x,
   inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))
 
 /- all propositions are Decidable -/
-noncomputable def propDecidable (a : Prop) : Decidable a :=
+@[scoped instance low] noncomputable def propDecidable (a : Prop) : Decidable a :=
   choice <| match em a with
     | Or.inl h => ⟨isTrue h⟩
     | Or.inr h => ⟨isFalse h⟩