aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
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"= " ++