Skip to content

Commit 140d100

Browse files
committed
make "Init.NotationExtra" import private
1 parent 8d5c6ed commit 140d100

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/Init/WFExtrinsicFix.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,10 @@ Authors: Paul Reichert
66
module
77

88
prelude
9+
public import Init.WF
910
import Init.Classical
1011
import Init.Ext
11-
public import Init.NotationExtra
12+
import Init.NotationExtra
1213

1314
set_option doc.verso true
1415
set_option linter.missingDocs true

0 commit comments

Comments
 (0)