diff options
Diffstat (limited to 'checker/checker.ml')
-rw-r--r-- | checker/checker.ml | 21 |
1 files changed, 18 insertions, 3 deletions
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") |