git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2461 from melted/issue_1134
cd4e91dNiklas Larsson
src/Idris/Elab/Clause.hs+1−1
compare with master
unifiedsplit
@@ -594,7 +594,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
594 rep <- useREPL
594 rep <- useREPL
595 when rep $ do
595 when rep $ do
596 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
596 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
597− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
597+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
598
598
599 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
599 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
600 -- Elaborate where block
600 -- Elaborate where block
src/Idris/Elab/Type.hs+1−1
@@ -148,7 +148,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
148 rep <- useREPL
148 rep <- useREPL
149 when rep $ do
149 when rep $ do
150 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
150 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
151− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
151+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
152
152
153 let (fam, _) = unApply (getRetTy nty')
153 let (fam, _) = unApply (getRetTy nty')
154 let corec = case fam of
154 let corec = case fam of