@@ -584,7 +584,8 @@ findLinear ist env tm | (P _ f _, args) <- unApply tm,
584 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)
584 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)
585 | Rig0 <- c = (a, c) : findLinArg sc as
585 | Rig0 <- c = (a, c) : findLinArg sc as
586 | Rig1 <- c = (a, c) : findLinArg sc as
586 | Rig1 <- c = (a, c) : findLinArg sc as
587− findLinArg (Bind n (Pi _ _ _ _) sc) (a : as) = findLinArg sc as
587+ findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)
588+ = findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as
588 findLinArg _ _ = []
589 findLinArg _ _ = []
589findLinear ist env (App _ f a)
590findLinear ist env (App _ f a)
590 = nub $ findLinear ist env f ++ findLinear ist env a
591 = nub $ findLinear ist env f ++ findLinear ist env a