From bf39064f298cfd7df966379af6f38110482bec7e Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 1 Feb 2007 19:43:27 +0000
Subject: Report de révision 9583 de la v8.1 dans le trunk

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9584 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b0f933a504..b395c0fd99 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -28,9 +28,12 @@ let w_refine ev rawc evd =
   let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    Pretyping.Default.understand_tcc (evars_of evd) env 
-      ~expected_type:e_info.evar_concl rawc in
-  evar_define ev typed_c (evars_reset_evd sigma evd)
+    try Pretyping.Default.understand_tcc (evars_of evd) env 
+      ~expected_type:e_info.evar_concl rawc 
+    with _ -> error ("The term is not well-typed in the environment of " ^
+			string_of_existential ev)
+  in
+    evar_define ev typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
 
-- 
cgit v1.2.3