diff options
| -rw-r--r-- | kernel/type_errors.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 14409c235a..5188093923 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -33,6 +33,7 @@ type type_error = | OccurCheck of int * constr | NotClean of int * constr | VarNotFound of identifier + | UnexpectedType of constr * constr | NotProduct of constr (* Pattern-matching errors *) | BadConstructor of constructor * inductive @@ -93,6 +94,9 @@ let error_not_inductive k env c = let error_ml_case k env mes c ct br brt = raise (TypeError (k, env, MLCase (mes,c,ct,br,brt))) +let error_unexpected_type env actual expected = + raise (TypeError (CCI, env, UnexpectedType (actual, expected))) + let error_not_product env c = raise (TypeError (CCI, env, NotProduct c)) |