@@ -1431,10 +1431,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1431 let (wbefore, wafter) = sepBlocks wb
1431 let (wbefore, wafter) = sepBlocks wb
1433 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1433 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1434− -- FIXME Changed info to winfo. Make sure that breaksn't things!
1435− -- - Changed it back for now; possibly want a differently
1436− -- modified ElabInfo.
1437− -- - Changed back back after modifying pinfo.
1438 mapM_ (elabDecl' EAll winfo) wbefore
1434 mapM_ (elabDecl' EAll winfo) wbefore
1439 -- Now build the RHS, using the type of the LHS as the goal.
1435 -- Now build the RHS, using the type of the LHS as the goal.
1440 i <- getIState -- new implicits from where block
1436 i <- getIState -- new implicits from where block