@@ -41,11 +41,10 @@ import Codec.Archive.Zip
4141import Util.Zlib (decompressEither)
4242
4343ibcVersion :: Word16
44−ibcVersion = 112
44+ibcVersion = 113
4545
4646data IBCFile = IBCFile { ver :: Word16,
4747 sourcefile :: FilePath,
48− symbols :: ![Name],
4948 ibc_imports :: ![(Bool, FilePath)],
5049 ibc_importdirs :: ![FilePath],
5150 ibc_implicits :: ![(Name, [PArg])],
@@ -95,7 +94,7 @@ deriving instance Binary IBCFile
9594!-}
9695
9796initIBC :: IBCFile
98−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
97+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
9998
10099loadIBC :: Bool -- ^ True = reexport, False = make everything private
101100 -> FilePath -> Idris ()
@@ -130,7 +129,6 @@ makeEntry name val = if L.null val
130129entries :: IBCFile -> [Entry]
131130entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),
132131 makeEntry "sourcefile" (sourcefile i),
133− makeEntry "symbols" (symbols i),
134132 makeEntry "ibc_imports" (ibc_imports i),
135133 makeEntry "ibc_importdirs" (ibc_importdirs i),
136134 makeEntry "ibc_implicits" (ibc_implicits i),
@@ -330,9 +328,7 @@ process reexp i fn = do
330328 pCGFlags =<< getEntry [] "ibc_cgflags" i
331329 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i
332330 pHdrs =<< getEntry [] "ibc_hdrs" i
333− symbols <- getEntry [] "symbols" i
334− defs <- getEntry [] "ibc_defs" i
335− pDefs reexp symbols defs
331+ pDefs reexp =<< getEntry [] "ibc_defs" i
336332 pPatdefs =<< getEntry [] "ibc_patdefs" i
337333 pAccess reexp =<< getEntry [] "ibc_access" i
338334 pFlags =<< getEntry [] "ibc_flags" i
@@ -485,8 +481,8 @@ pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
485481pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
486482 i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
487483
488−pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()
489−pDefs reexp syms ds
484+pDefs :: Bool -> [(Name, Def)] -> Idris ()
485+pDefs reexp ds
490486 = mapM_ (\ (n, d) ->
491487 do d' <- updateDef d
492488 case d' of