@@ -618,8 +618,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
618618 (tmv, tmt) <- lift $ check ctxt env tm
619619 let tmt' = normalise ctxt env tmt
620620 let (tacn, tacstr, tactt) = if induction
621− then (ElimN, "an eliminator", "induction")
622− else (CaseN, "a case function", "case analysis")
621+ then (ElimN, "an eliminator", "Induction")
622+ else (CaseN, "a case function", "Case analysis")
623623 case unApply tmt' of
624624 (P _ tnm _, tyargs) -> do
625625 case lookupTy (SN (tacn tnm)) ctxt of
@@ -653,8 +653,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
653653 (scv, sct) <- lift $ check ctxt env res'
654654 let (scv', _) = specialise ctxt env [] scv
655655 return scv'
656− [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
657− xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
656+ [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
657+ xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
658658 _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
659659 where scname = sMN 0 "scarg"
660660 makeConsArg (nm, ty) = P Bound nm ty