From bbaf95ab41d91c5cd308308c07d8620a4d96649a Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 6 Sep 2000 12:52:16 +0000
Subject: Ajout erreur unexpected type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@584 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/type_errors.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/type_errors.ml')

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))
 
-- 
cgit v1.2.3