aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-21 18:19:46 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-26 14:53:08 +0100
commitf1e1452841997c08217bd4caf1da8370f17c93f3 (patch)
tree457833423fdc28e0af5252cfc87a59ee4bb31af9
parent23a33c1a7781e35faf83ed4c7e42df8c8803e64e (diff)
checker: less useless error messages
-rw-r--r--checker/checker.ml21
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")