@@ -66,8 +66,6 @@ inaccessibleImps _ _ _ = []
67-- | Get the list of (index, name) of inaccessible arguments from the type.
67-- | Get the list of (index, name) of inaccessible arguments from the type.
68inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
68inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
69−inaccessibleArgs i (PPi (Imp _ _ _ _) n _ Placeholder t)
70− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
71inaccessibleArgs i (PPi plicity n _ ty t)
69inaccessibleArgs i (PPi plicity n _ ty t)
72 | InaccessibleArg `elem` pargopts plicity
70 | InaccessibleArg `elem` pargopts plicity
73 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
71 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}