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

4 files changed, 9 insertions, 6 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 22251aabbc..326f8222ef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -630,6 +630,10 @@ let check_projection isproj nargs r =
   | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
   | _, None -> ()
 
+let get_implicit_name n imps =
+  if !Options.v7 then None
+  else Some (Impargs.name_of_implicit (List.nth imps (n-1)))
+
 let set_hole_implicit i = function
   | RRef (loc,r) -> (loc,ImplicitArg (r,i))
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
@@ -982,7 +986,7 @@ let internalise sigma env allow_soapp lvar c =
 	    (* with implicit arguments *)
 	    []
 	  else
-	    RHole (set_hole_implicit n c) :: 
+	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
 	      aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 47edc73cea..1aeca07cb7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -49,7 +49,7 @@ type 'a bindings =
 type 'a with_bindings = 'a * 'a bindings
 
 type hole_kind =
-  | ImplicitArg of global_reference * int
+  | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
   | QuestionMark
   | CasesType
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 29237a675b..54bb306bd0 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -47,7 +47,7 @@ type 'a bindings =
 type 'a with_bindings = 'a * 'a bindings
 
 type hole_kind =
-  | ImplicitArg of global_reference * int
+  | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
   | QuestionMark
   | CasesType
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