Amélioration des messages d'erreurs concernant l'inférence des implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 4 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2d93c6fd3..4041d311c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -95,10 +95,14 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
 let explain_case_not_inductive ctx cj =
   let pc = prterm_env ctx cj.uj_val in
   let pct = prterm_env ctx cj.uj_type in
-  str "In Cases expression, the matched term" ++ brk(1,1) ++ pc ++ spc () ++ 
-  str "has type" ++ brk(1,1) ++ pct ++ spc () ++ 
-  str "which is not a (co-)inductive type"
-  
+    match kind_of_term cj.uj_type with
+      | Evar _ -> 
+	  str "Cannot infer a type for this expression"
+      | _ ->
+	  str "This term" ++ brk(1,1) ++ pc ++ spc () ++ 
+	  str "has type" ++ brk(1,1) ++ pct ++ spc () ++ 
+	  str "which is not a (co-)inductive type"
+
 let explain_number_branches ctx cj expn =
   let pc = prterm_env ctx cj.uj_val in
   let pct = prterm_env ctx cj.uj_type in