git.iko.soy/Idris-dev
on master help sign in
Fix import public error
f56f05eEdwin Brady
libs/contrib/Data/Fun.idr+1−1
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1module Data.Fun
1module Data.Fun
2
2
3−import Data.Vect
3+import public Data.Vect
4
4
5%default total
5%default total
6
6
src/Idris/IBC.hs+4−4
@@ -312,7 +312,7 @@ process reexp i fn = do
312 srcok <- runIO $ doesFileExist source
312 srcok <- runIO $ doesFileExist source
313 when srcok $ timestampOlder source fn
313 when srcok $ timestampOlder source fn
314 pImportDirs =<< getEntry [] "ibc_importdirs" i
314 pImportDirs =<< getEntry [] "ibc_importdirs" i
315− pImports =<< getEntry [] "ibc_imports" i
315+ pImports reexp =<< getEntry [] "ibc_imports" i
316 pImps =<< getEntry [] "ibc_implicits" i
316 pImps =<< getEntry [] "ibc_implicits" i
317 pFixes =<< getEntry [] "ibc_fixes" i
317 pFixes =<< getEntry [] "ibc_fixes" i
318 pStatics =<< getEntry [] "ibc_statics" i
318 pStatics =<< getEntry [] "ibc_statics" i
@@ -383,8 +383,8 @@ pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns
383pImportDirs :: [FilePath] -> Idris ()
383pImportDirs :: [FilePath] -> Idris ()
384pImportDirs fs = mapM_ addImportDir fs
384pImportDirs fs = mapM_ addImportDir fs
385
385
386−pImports :: [(Bool, FilePath)] -> Idris ()
386+pImports :: Bool -> [(Bool, FilePath)] -> Idris ()
387−pImports fs
387+pImports reexp fs
388 = do mapM_ (\(re, f) ->
388 = do mapM_ (\(re, f) ->
389 do i <- getIState
389 do i <- getIState
390 ibcsd <- valIBCSubDir i
390 ibcsd <- valIBCSubDir i
@@ -398,7 +398,7 @@ pImports fs
398 ifail "Must be an ibc"
398 ifail "Must be an ibc"
399 IDR fn -> do logLvl 1 $ "Failed at " ++ fn
399 IDR fn -> do logLvl 1 $ "Failed at " ++ fn
400 ifail "Must be an ibc"
400 ifail "Must be an ibc"
401− IBC fn src -> loadIBC re fn)
401+ IBC fn src -> loadIBC (reexp && re) fn)
402 fs
402 fs
403
403
404pImps :: [(Name, [PArg])] -> Idris ()
404pImps :: [(Name, [PArg])] -> Idris ()
test/dsl002/Resimp.idr+1−1
@@ -1,6 +1,6 @@
1module Resimp
1module Resimp
2
2
3−import Data.Vect
3+import public Data.Vect
4import public Data.Fin
4import public Data.Fin
5
5
6-- IO operations which read a resource
6-- IO operations which read a resource