From f0a1cccebe0a969ff707623b8f74e8c3559386e0 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 11 Nov 2024 09:26:27 +0100 Subject: [PATCH] maybe this import should go? --- ImportGraph.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/ImportGraph.lean b/ImportGraph.lean index a58f13b..183f1ac 100644 --- a/ImportGraph.lean +++ b/ImportGraph.lean @@ -3,4 +3,3 @@ import ImportGraph.Imports import ImportGraph.CurrentModule import ImportGraph.Lean.Name import ImportGraph.RequiredModules -import ImportGraph.UnusedTransitiveImports