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/typeops.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'kernel/typeops.ml')

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