git.iko.soy/Idris-dev
on master help sign in
Remember to save deferred definition types in IBC

Partial fix for #955 (still need to save missing case information, though this is less important)

commit3bb32737c5d43525320c47915628968190bb1e15 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 21 Mar 2014, 13:40 (13 years ago) parentc5cb67c
1 file changed+1
compare with master
unifiedsplit
src/Idris/ElabDecls.hs+1
src/Idris/ElabDecls.hs+1
@@ -1461,6 +1461,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14611461 def' <- checkDef fc defer
14621462 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
14631463 addDeferred def''
1464+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
14641465
14651466 when (not (null def')) $ do
14661467 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')