git.iko.soy/Idris-dev
on master help sign in
Wrap data declarations in mutual blocks
c56dee3David Raymond Christiansen
src/Idris/Coverage.hs+1−1
compare with master
unifiedsplit
@@ -705,7 +705,7 @@ checkMP ist i mp = if i > 0
705 = case lookupTotal f (tt_ctxt ist) of
705 = case lookupTotal f (tt_ctxt ist) of
706 [Total _] -> Unchecked -- okay so far
706 [Total _] -> Unchecked -- okay so far
707 [Partial _] -> Partial (Other [f])
707 [Partial _] -> Partial (Other [f])
708− x -> error $ "CAN'T HAPPEN: " ++ (show x)
708+ x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
709 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
709 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
710 = Total []
710 = Total []
711 tryPath desc path (e@(f, args) : es) arg
711 tryPath desc path (e@(f, args) : es) arg
src/Idris/Parser.hs+1
@@ -1471,6 +1471,7 @@ loadSource lidr f toline
1471 case x of
1471 case x of
1472 PClauses{} -> r
1472 PClauses{} -> r
1473 PClass{} -> r
1473 PClass{} -> r
1474+ PData{} -> r
1474 PInstance{} -> r
1475 PInstance{} -> r
1475 _ -> x
1476 _ -> x
1476
1477