aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-22 14:24:25 +0100
committerGaëtan Gilbert2019-03-11 13:36:03 +0100
commitab1fd660db052741a3d9aed871251dc3dbee63ca (patch)
tree43e020254a6862d4174e96fb3f24c31395e9a1c1 /checker
parent7d436786e79b79643999cddff70f5fbf3b4c3ad9 (diff)
Nicer error for bad primitive types (through type_errors etc)
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 3c93ef7d36..d3f346d76b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -273,6 +273,7 @@ let explain_exn = function
| IllFormedBranch _ -> str"IllFormedBranch"
| Generalization _ -> str"Generalization"
| ActualType _ -> str"ActualType"
+ | IncorrectPrimitive _ -> str"IncorrectPrimitive"
| CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) ->
let pp_arg i judge =
hv 1 (str"arg " ++ int (i+1) ++ str"= " ++