From f1e1452841997c08217bd4caf1da8370f17c93f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 21 Feb 2014 18:19:46 +0100 Subject: checker: less useless error messages --- checker/checker.ml | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'checker/checker.ml') diff --git a/checker/checker.ml b/checker/checker.ml index d54e9328a..1bdd0f0e2 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -261,9 +261,24 @@ let rec explain_exn = function mt() in hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> -(* hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *) - (* te)*) - hov 0 (str "Type error") + hov 0 (str "Type error: " ++ + (match te with + | UnboundRel i -> str"UnboundRel " ++ int i + | UnboundVar v -> str"UnboundVar" ++ str(Names.Id.to_string v) + | NotAType _ -> str"NotAType" + | BadAssumption _ -> str"BadAssumption" + | ReferenceVariables _ -> str"ReferenceVariables" + | ElimArity _ -> str"ElimArity" + | CaseNotInductive _ -> str"CaseNotInductive" + | WrongCaseInfo _ -> str"WrongCaseInfo" + | NumberBranches _ -> str"NumberBranches" + | IllFormedBranch _ -> str"IllFormedBranch" + | Generalization _ -> str"Generalization" + | ActualType _ -> str"ActualType" + | CantApplyBadType _ -> str"CantApplyBadType" + | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" + | IllFormedRecBody _ -> str"IllFormedRecBody" + | IllTypedRecBody _ -> str"IllTypedRecBody")) | Indtypes.InductiveError e -> hov 0 (str "Error related to inductive types") -- cgit v1.2.3