From bbfc54ebeeac8ccee9fd7ad2d379d4741ce3335d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jun 2000 15:16:53 +0000
Subject: Amelioration messages erreurs

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

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 07083d7a2c..13cd80a685 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -196,7 +196,9 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
 		  (try 
 		     inh_conv_coerce_to_fail env isevars c1 hj 
 		   with NoCoercion ->
-                     error_cant_apply_bad_type_loc apploc env (n,c1,body_of_type hj.uj_type)
+                     error_cant_apply_bad_type_loc apploc env 
+		       (n,nf_ise1 !isevars c1,
+			nf_ise1 !isevars (body_of_type hj.uj_type))
 		       (j_nf_ise env !isevars funj)
 		       (jl_nf_ise env !isevars argjl)) 
 	      in
-- 
cgit v1.2.3