diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 1e0e3e8f3363..ee45526b29a9 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura Notation for operators defined at Prelude.lean -/ prelude -import Init.NotationExtra +import Init.Meta namespace Lean.Parser.Tactic.Conv diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index a5f1912fb416..c07abb6cdeaf 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -4,11 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import Init.Control.Except import Init.Data.ByteArray -import Init.SimpLemmas -import Init.Util -import Init.WFTactics namespace String