diff options
| author | herbelin | 2004-08-23 12:58:27 +0000 |
|---|---|---|
| committer | herbelin | 2004-08-23 12:58:27 +0000 |
| commit | e07c4d7d7545652ee0e5f2cd05c53b45f92e0df6 (patch) | |
| tree | 22b06756e26a7186b2f9079e32d1dd5870fc7372 /toplevel | |
| parent | 0b18e84d1fc34dd098dfff91e83d795ce41bb774 (diff) | |
Correction bug #830 : les noms des implicites temporaires étaient inconnus au moment de l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9d2160cb68..01f69ce05c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -323,13 +323,12 @@ let explain_hole_kind env = function str "a type for " ++ Nameops.pr_id id | BinderType Anonymous -> str "a type for this anonymous binder" - | ImplicitArg (c,n) -> + | ImplicitArg (c,(n,ido)) -> if !Options.v7 then str "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 + let id = out_some ido in str "an instance for the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c |