diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 10:24:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 10:24:07 +0000 |
| commit | bc9f28dfba3a93151d26de582a858624cd266960 (patch) | |
| tree | ea56b958fb07fbacad41a9f7369c02219f1a368a /toplevel/himsg.ml | |
| parent | 78c1f8921ccbbdf6c7114ae8519e6a860f99ec6f (diff) | |
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
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e8fd76e43..9bb8d34c7 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) -> |