@@ -286,7 +286,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
286 -- block reduction immediately under codata (and not forced)
286 -- block reduction immediately under codata (and not forced)
287 ev ntimes stk top env
287 ev ntimes stk top env
288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
289− | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
289+ | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)
290 = do let (f, _) = unApply arg
290 = do let (f, _) = unApply arg
291 let ntimes' = case f of
291 let ntimes' = case f of
292 P _ fn _ -> (fn, 0) : ntimes
292 P _ fn _ -> (fn, 0) : ntimes