diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 681588ee17..e16e3703b6 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -12,7 +12,7 @@ public import all Std.Data.DHashMap.Internal.Defs public import Std.Data.DHashMap.Internal.HashesTo public import Std.Data.DHashMap.Internal.AssocList.Lemmas -public @[expose] section +@[expose] public section /-! This is an internal implementation file of the hash map. Users of the hash map should not rely on diff --git a/src/Std/Internal/Rat.lean b/src/Std/Internal/Rat.lean index 84a97ceb08..e17ef0defb 100644 --- a/src/Std/Internal/Rat.lean +++ b/src/Std/Internal/Rat.lean @@ -12,7 +12,7 @@ public import Init.Data.Int.DivMod.Basic public import Init.Data.Int.Linear public import Init.Data.Nat.Gcd -public @[expose] section +@[expose] public section namespace Std namespace Internal diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean index 683eefb5c1..efd391b7b0 100644 --- a/src/Std/Time/Internal/Bounded.lean +++ b/src/Std/Time/Internal/Bounded.lean @@ -10,7 +10,7 @@ public import Init.Omega public import Init.Data.Int.DivMod.Lemmas public import Std.Classes.Ord.Basic -public @[expose] section +@[expose] public section namespace Std namespace Time diff --git a/src/Std/Time/Internal/UnitVal.lean b/src/Std/Time/Internal/UnitVal.lean index 0e08b53aba..7f9d3335c7 100644 --- a/src/Std/Time/Internal/UnitVal.lean +++ b/src/Std/Time/Internal/UnitVal.lean @@ -9,7 +9,7 @@ prelude public import Std.Classes.Ord.Basic public import Std.Internal.Rat -public @[expose] section +@[expose] public section namespace Std namespace Time diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean index 3fd4aaa803..646e0c978d 100644 --- a/src/Std/Time/Time/Unit/Second.lean +++ b/src/Std/Time/Time/Unit/Second.lean @@ -9,7 +9,7 @@ prelude public import Std.Internal.Rat public import Std.Time.Time.Unit.Nanosecond -public @[expose] section +@[expose] public section namespace Std namespace Time