max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reduce dependencies

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-16 19:45:45 +01:00
parent eb25b97501
commit fcb1616c20
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/InfoUtils.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki
-/
import Lean.Elab
import Lean.Elab.InfoTree
namespace Lean.Elab