@@ -132,7 +132,9 @@ induction subj =
132132 (_, ty) <- check !getEnv subj
133133 ty' <- forget ty
134134 case headName ty' of
135− Nothing => fail [TermPart ty, TextPart "is not an inductive family"]
135+ Nothing =>
136+ fail [TermPart ty,
137+ TextPart "is not a datatype declared with the data keyword"]
136138 Just fam =>
137139 do let elim = elimN fam
138140 (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim