@@ -618,8 +618,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
618 (tmv, tmt) <- lift $ check ctxt env tm
618 (tmv, tmt) <- lift $ check ctxt env tm
619 let tmt' = normalise ctxt env tmt
619 let tmt' = normalise ctxt env tmt
620 let (tacn, tacstr, tactt) = if induction
620 let (tacn, tacstr, tactt) = if induction
621− then (ElimN, "an eliminator", "induction")
621+ then (ElimN, "an eliminator", "Induction")
622− else (CaseN, "a case function", "case analysis")
622+ else (CaseN, "a case function", "Case analysis")
623 case unApply tmt' of
623 case unApply tmt' of
624 (P _ tnm _, tyargs) -> do
624 (P _ tnm _, tyargs) -> do
625 case lookupTy (SN (tacn tnm)) ctxt of
625 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
653 (scv, sct) <- lift $ check ctxt env res'
653 (scv, sct) <- lift $ check ctxt env res'
654 let (scv', _) = specialise ctxt env [] scv
654 let (scv', _) = specialise ctxt env [] scv
655 return scv'
655 return scv'
656− [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
656+ [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
657− xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
657+ xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
658 _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
658 _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
659 where scname = sMN 0 "scarg"
659 where scname = sMN 0 "scarg"
660 makeConsArg (nm, ty) = P Bound nm ty
660 makeConsArg (nm, ty) = P Bound nm ty