@@ -1505,6 +1505,19 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15051505 addErrRev (crhs, clhs)
15061506 return $ Right (clhs, crhs)
15071507 where
1508+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
1509+ pinfo info ns ds i
1510+ = let newps = params info ++ ns
1511+ dsParams = map (\n -> (n, map fst newps)) ds
1512+ newb = addAlist dsParams (inblock info)
1513+ l = liftname info in
1514+ info { params = newps,
1515+ inblock = newb,
1516+ liftname = id -- (\n -> case lookupCtxt n newb of
1517+ -- Nothing -> n
1518+ -- _ -> MN i (show n)) . l
1519+ }
1520+
15081521 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
15091522 mkLHSapp t = t
15101523
@@ -2157,18 +2170,6 @@ psolve tm = return ()
21572170pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc
21582171pvars ist _ = []
21592172
2160−pinfo info ns ds i
2161− = let newps = params info ++ ns
2162− dsParams = map (\n -> (n, map fst newps)) ds
2163− newb = addAlist dsParams (inblock info)
2164− l = liftname info in
2165− info { params = newps,
2166− inblock = newb,
2167− liftname = id -- (\n -> case lookupCtxt n newb of
2168− -- Nothing -> n
2169− -- _ -> MN i (show n)) . l
2170− }
2171−
21722173data ElabWhat = ETypes | EDefns | EAll
21732174 deriving (Show, Eq)
21742175