Correction du bug #1116

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

3 files changed, 19 insertions, 30 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6196c4ecef..7664998224 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -278,6 +278,14 @@ let find_name decl gl = function
       if id' <> id then error ((string_of_id id)^" is already used");
       id'
 
+let find_intro_names ctxt gl = 
+  List.rev 
+    (List.fold_right 
+    (fun decl idl -> find_name decl gl (IntroAvoid idl)::idl)
+    ctxt
+    [])
+
+
 let build_intro_tac id = function
   | None      -> introduction id
   | Some dest -> tclTHEN (introduction id) (move_hyp true id dest)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f5355eba13..9411a772bf 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -58,6 +58,7 @@ val cofix           : identifier option -> tactic
 (*s Introduction tactics. *)
 
 val fresh_id : identifier list -> identifier -> goal sigma -> identifier
+val find_intro_names : rel_context -> goal sigma -> identifier list
 
 val intro                : tactic
 val introf               : tactic
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5c0ac05f0c..29f3b321f6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -111,39 +111,19 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 
   (* Simulate the Intro(s) tactic *)
 
-let fresh_id_of_name avoid gl = function
-    Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
-  | Name id   -> Tactics.fresh_id avoid id gl
-
-let rec do_renum avoid gl = function
-    [] -> mt ()
-  | [n] -> pr_id (fresh_id_of_name avoid gl n)
-  | n :: l ->
-      let id = fresh_id_of_name avoid gl n in
-      pr_id id ++ spc () ++ do_renum (id :: avoid) gl l
-
-(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *)
-let decompose_prod_letins = 
-  let rec prodec_rec l c = match kind_of_term c with
-    | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c
-    | Cast (c,_,_)   -> prodec_rec l c
-    | _              -> l,c
-  in 
-  prodec_rec []
-
 let show_intro all =
   let pf = get_pftreestate() in
   let gl = nth_goal_of_pftreestate 1 pf in
-  let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in
-  let nl = List.rev_map fst l in
-  if all then msgnl (hov 0 (do_renum [] gl nl))
-  else try 
-    let n = List.hd nl in
-    msgnl (pr_id (fresh_id_of_name [] gl n))
-  with Failure "hd" -> message "" 
-
+  let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+  if all 
+  then 
+    let lid = Tactics.find_intro_names l gl in 
+    msgnl (hov 0 (prlist_with_sep  spc pr_id lid))
+  else  
+    try  
+      let n = list_last l in
+      msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+    with Failure "list_last" -> message ""
 
 let id_of_name = function 
   | Names.Anonymous -> id_of_string "x"