@@ -528,13 +528,19 @@ elab ist info pattern tcgen fn tm
528 -- old ones with an _
528 -- old ones with an _
529 mkClause args (l, r)
529 mkClause args (l, r)
530 = let args' = map (shadowed (allNamesIn l)) args
530 = let args' = map (shadowed (allNamesIn l)) args
531− lhs = PApp fc (PRef fc n)
531+ lhs = PApp (getFC fc l) (PRef (getFC fc l) n)
532 (map pexp args' ++ [pexp l]) in
532 (map pexp args' ++ [pexp l]) in
533+-- trace (show (getFC fc l, getFC fc r)) $
533− PClause fc n lhs [] r []
534+ PClause (getFC fc l) n lhs [] r []
535 shadowed new (PRef _ n) | n `elem` new = Placeholder
536 shadowed new (PRef _ n) | n `elem` new = Placeholder
536 shadowed new t = t
537 shadowed new t = t
539+ getFC d (PApp fc _ _) = fc
540+ getFC d (PRef fc _) = fc
541+ getFC d (PAlternative _ (x:_)) = getFC d x
538 insertCoerce ina t =
544 insertCoerce ina t =
539 do ty <- goal
545 do ty <- goal
540 -- Check for possible coercions to get to the goal
546 -- Check for possible coercions to get to the goal