@@ -268,9 +268,14 @@ elabClauses info' fc opts n_in cs =
268 -- 'Partial NotCovering'
268 -- 'Partial NotCovering'
269 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
269 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
271− noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
271+ noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
272 Right _ -> False
272 Right _ -> False
273 Left miss -> True) cs
273 Left miss -> True) cs
275+ trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)
276+ = let args = min (length ls) (length rs) in
277+ matchClause i (PApp fcl fl (take args ls))
278+ (PApp fcr fr (take args rs))
275 checkUndefined n ctxt = case lookupDef n ctxt of
280 checkUndefined n ctxt = case lookupDef n ctxt of
276 [] -> return ()
281 [] -> return ()