diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 12:52:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 12:52:16 +0000 |
| commit | bbaf95ab41d91c5cd308308c07d8620a4d96649a (patch) | |
| tree | 2742de3ace6959a82a65a2ad636563f17ccc6d6f /kernel/type_errors.ml | |
| parent | 8ec12027e4641f88272c0275e31e93565f7c34cc (diff) | |
Ajout erreur unexpected type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
| -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 14409c235..518809392 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)) |