From bc9f28dfba3a93151d26de582a858624cd266960 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 10:24:07 +0000
Subject: Utilisation nom dans message d'erreur implicite pas trouve

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5020 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e8fd76e43f..9bb8d34c78 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -328,8 +328,15 @@ let explain_unsolvable_implicit env = function
   | BinderType Anonymous ->
       str "Cannot infer a type for this anonymous binder"
   | ImplicitArg (c,n) ->
-      str "Cannot infer the " ++ pr_ord n ++
-      str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
+      if !Options.v7 then
+	str "Cannot infer the " ++ pr_ord n ++
+	str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
+      else
+	let imps = Impargs.implicits_of_global c in
+	let id = Impargs.name_of_implicit (List.nth imps (n-1)) in
+	str "Unable to infer an instance for the implicit parameter " ++
+	pr_id id ++ spc () ++ str "of" ++
+	spc () ++ Nametab.pr_global_env Idset.empty c
   | InternalHole ->
       str "Cannot infer a term for an internal placeholder"
   | TomatchTypeParameter (tyi,n) ->
-- 
cgit v1.2.3