Merge pull request #2461 from melted/issue_1134
Fix #1134 by saving same info in ibc on check
commitcd4e91d9d3fde79534c0fa9c07fc2836173cf98a
authorNiklas Larsson <metaniklas@gmail.com>
dateThu 23 Jul 2015, 19:33 (11 years ago)
parent4cd8854585627b
src/Idris/Elab/Clause.hs+1−1
@@ -594,7 +594,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
594594 rep <- useREPL
595595 when rep $ do
596596 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))
598598
599599 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
600600 -- 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
148148 rep <- useREPL
149149 when rep $ do
150150 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')))
152152
153153 let (fam, _) = unApply (getRetTy nty')
154154 let corec = case fam of