From 09c4af26fce85559202a9c8a65837da88fefcd5e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jun 2022 16:41:54 -0700
Subject: [PATCH] fix: `ConstantInfo.all` for consistency

---
 src/Lean/Declaration.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 30336c054f..29747fc285 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -417,7 +417,7 @@ def all : ConstantInfo → List Name
   | defnInfo val   => val.all
   | thmInfo val    => val.all
   | opaqueInfo val => val.all
-  | _              => []
+  | info           => [info.name]
 
 @[extern "lean_instantiate_type_lparams"]
 opaque instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr