ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 22:47:12 +03:00
Code Issues Projects Releases Wiki Activity

Fix #1134 by saving same info in ibc on check

Browse Source 
Otherwise addClause will fail as the ibc lacks that info
This commit is contained in:
Niklas Larsson 2015-07-23 18:09:21 +02:00
parent f48665eb51
commit 585627b6ca
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/Elab/Clause.hs
View File

@ -594,7 +594,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
rep <- useREPL
when rep $ do
addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
-- Elaborate where block

2
src/Idris/Elab/Type.hs
View File

@ -148,7 +148,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
rep <- useREPL
when rep $ do
addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
let (fam, _) = unApply (getRetTy nty')
let corec = case fam of