From 0228f9c9b703ee675cdbe792fdea85ebdb6ce387 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jan 2020 12:08:20 -0800 Subject: [PATCH] chore: remove `addMacroScopeExt` --- src/Init/LeanInit.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index a170a90f8c..67ede337b7 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -256,9 +256,6 @@ We use two delimiters for improving `hasMacroScopes` performance. private def mkMacroScopeName (mainModule : Name) (n : Name) : Name := mkNameStr (mkNameStr n "_@" ++ mainModule) "_hyg" -def addMacroScopeExt (mainModule : Name) (n : Name) (scp : MacroScope) : Name := -mkNameNum (mkMacroScopeName mainModule n) scp - def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name := mkNameNum (mkMacroScopeName mainModule n) scp