@@ -286,17 +286,17 @@ 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
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
293 _ -> ntimes
293 _ -> ntimes
294− when (spec || simpl) $ setBlock True
294+ when spec $ setBlock True
295 d' <- ev ntimes' stk False env d
295 d' <- ev ntimes' stk False env d
296 l' <- ev ntimes' stk False env l
296 l' <- ev ntimes' stk False env l
297 t' <- ev ntimes' stk False env t
297 t' <- ev ntimes' stk False env t
298 arg' <- ev ntimes' stk False env arg
298 arg' <- ev ntimes' stk False env arg
299− when (spec || simpl) $ setBlock False
299+ when spec $ setBlock False
300 evApply ntimes' stk top env [l',t',arg'] d'
300 evApply ntimes' stk top env [l',t',arg'] d'
301 -- Treat "assert_total" specially, as long as it's defined!
301 -- Treat "assert_total" specially, as long as it's defined!
302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)