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

3 files changed, 24 insertions, 13 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 8ca7135aa5..a4661433e1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -22,7 +22,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
@@ -73,8 +75,11 @@ let error_generalization k env nvar c =
 let error_actual_type k env c actty expty =
   raise (TypeError (k, context env, ActualType (c,actty,expty)))
 
-let error_cant_apply k env s rator randl =
-  raise (TypeError (k, context env, CantAply (s,rator,randl)))
+let error_cant_apply_not_functional k env rator randl =
+  raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl)))
+
+let error_cant_apply_bad_type k env t rator randl =
+  raise (TypeError (k, context env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body k env str lna i vdefs =
   raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs)))
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
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6c7e1bbe5e..1a6c1d885f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -317,7 +317,7 @@ let cast_rel env sigma cj tj =
 (* Type of an application. *)
 
 let apply_rel_list env sigma nocheck argjl funj =
-  let rec apply_rec typ cst = function
+  let rec apply_rec n typ cst = function
     | [] -> 
 	{ uj_val  = applist (j_val_only funj, List.map j_val_only argjl);
           uj_type = typ;
@@ -327,18 +327,19 @@ let apply_rel_list env sigma nocheck argjl funj =
         match whd_betadeltaiota env sigma typ with
           | DOP2(Prod,c1,DLAM(_,c2)) ->
               if nocheck then
-                apply_rec (subst1 hj.uj_val c2) cst restjl
+                apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl
 	      else 
 		(try 
 		   let c = conv_leq env sigma hj.uj_type c1 in
 		   let cst' = Constraint.union cst c in
-		   apply_rec (subst1 hj.uj_val c2) cst' restjl
+		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
 		 with NotConvertible -> 
-		   error_cant_apply CCI env "Type Error" funj argjl)
+		   error_cant_apply_bad_type CCI env (n,hj.uj_type,c1)
+		     funj argjl)
           | _ ->
-              error_cant_apply CCI env "Non-functional construction" funj argjl
+	      error_cant_apply_not_functional CCI env funj argjl
   in 
-  apply_rec funj.uj_type Constraint.empty argjl
+  apply_rec 1 funj.uj_type Constraint.empty argjl
 
 
 (* Fixpoints. *)