diff options
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |