From 01c61a9fdc76d4743a4ba23fd4b76acc5d6adef5 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Mon, 23 Oct 2006 08:42:44 +0000
Subject: Fixed "Show intros" which did not look at hypothesis.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9260 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 433b64c326..2befb7e42e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -291,9 +291,8 @@ let find_intro_names ctxt gl =
     (fun decl acc -> 
       let wantedname,x,typdecl = decl in
       let env,idl = acc in
-      let name = fresh_id_avoid idl (default_id env gl.sigma decl) in
+      let name = fresh_id idl (default_id env gl.sigma decl) gl in
       let newenv = push_rel (wantedname,x,typdecl) env in
-      (* 	let newgl = List.hd ((fst (intro gl)).) in *)
       (newenv,(name::idl)))
     ctxt (pf_env gl , []) in
   List.rev res 
-- 
cgit v1.2.3