From ab1fd660db052741a3d9aed871251dc3dbee63ca Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 22 Feb 2019 14:24:25 +0100
Subject: Nicer error for bad primitive types (through type_errors etc)

---
 kernel/type_errors.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 4b832930e1..c5ab9a4e73 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -56,6 +56,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
   | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
   | ActualType of ('constr, 'types) punsafe_judgment * 'types
+  | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -112,6 +113,8 @@ val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
 
 val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
+val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a
+
 val error_cant_apply_not_functional :
   env -> unsafe_judgment -> unsafe_judgment array -> 'a
 
-- 
cgit v1.2.3