From faf07e58db60389b91ed372fba74a08279869828 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 4 Dec 2024 13:46:08 +0100
Subject: [PATCH] chore: remove unused imports (#6305)

This PR removes an unused import in the time library that can yield to
import cycles when building stuff that gets imported by `Std.Internal`
but also wants to import `Std.Time`.
---
 src/Std/Time/Zoned/DateTime.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean
index 8082a6da89..4f69cda6ce 100644
--- a/src/Std/Time/Zoned/DateTime.lean
+++ b/src/Std/Time/Zoned/DateTime.lean
@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 prelude
 import Std.Time.DateTime
 import Std.Time.Zoned.TimeZone
-import Std.Internal
 
 namespace Std
 namespace Time