From 2372cbdcabec698e5deb5abfc393ed3e6909995f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 May 2000 15:57:50 +0000
Subject: Modification messages d'erreurs, possibilité de n'importe quel constr
 dans les instances de références

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

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 7ffbd312e8..a975419807 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -24,7 +24,9 @@ type type_error =
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * typed_type) * constr
   | ActualType of constr * constr * constr
-  | CantAply of string * unsafe_judgment * unsafe_judgment list
+  | CantApplyBadType of (int * constr * constr)
+      * unsafe_judgment * unsafe_judgment list
+  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
@@ -71,9 +73,12 @@ val error_generalization :
 val error_actual_type :
   path_kind -> env -> constr -> constr -> constr -> 'b
 
-val error_cant_apply : 
-  path_kind -> env -> string -> unsafe_judgment 
-    -> unsafe_judgment list -> 'b
+val error_cant_apply_not_functional : 
+  path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'b
+
+val error_cant_apply_bad_type : 
+  path_kind -> env -> int * constr * constr -> 
+      unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_ill_formed_rec_body :
   path_kind -> env -> std_ppcmds
-- 
cgit v1.2.3