@@ -124,7 +124,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
124124 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
125125 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
126126
127− checkDefinedAs fc n t ctxt
127+ checkDefinedAs fc n t ctxt
128128 = case lookupDef n ctxt of
129129 [] -> return ()
130130 [TyDecl _ ty] ->
@@ -204,14 +204,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
204204 liftname = id -- Is this appropriate?
205205 }
206206
207−-- FIXME: 'forcenames' is an almighty hack! Need a better way of
208−-- erasing non-forceable things
209−-- ^^^
210−-- TODO: the above is a comment from the past;
211−-- forcenames is probably no longer needed
212207elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
213208 Type -> -- for kind checking
214− (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->
209+ (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->
215210 Idris (Name, Type)
216211elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
217212 = do checkUndefined fc n
@@ -244,7 +239,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
244239 else return ()
245240 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
246241
247− mkLazy (PPi pl n ty sc)
242+ mkLazy (PPi pl n ty sc)
248243 = let ty' = if getTyName ty
249244 then PApp fc (PRef fc (sUN "Lazy'"))
250245 [pexp (PRef fc (sUN "LazyCodata")),
@@ -417,7 +412,7 @@ elabCaseFun ind paramPos n ty cons info = do
417412 case findIndex (== n) oldParams of
418413 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
419414 Just i -> (removeParamPis oldParams params tyr)
420− removeParamPis oldParams params (PRef _ n) =
415+ removeParamPis oldParams params (PRef _ n) =
421416 case findIndex (== n) oldParams of
422417 Nothing -> (PRef elimFC n)
423418 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
@@ -518,4 +513,3 @@ elabCaseFun ind paramPos n ty cons info = do
518513 where applyRecElim :: (Name, Plicity, PTerm) -> PArg
519514 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
520515 where (_, idxs) = splitArgPms recTy
521−