@@ -49,12 +49,12 @@ names over '_', patterns over names, etc.
4949-- variable updates
5050split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
5151split n t'
52− = do (tm, ty, pats) <- elabValBind toplevel True t'
52+ = do ist <- getIState
53+ (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
5354 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
54− ist <- getIState
5555-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
5656-- iputStrLn (show pats)
57− let t = mergeUserImpl (addImpl ist t') (delab ist tm) -- addImplPat ist t'
57+ let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
5858 let ctxt = tt_ctxt ist
5959 case lookup n pats of
6060 Nothing -> fail $ show n ++ " is not a pattern variable"