diff options
| author | courtieu | 2006-10-23 08:42:44 +0000 |
|---|---|---|
| committer | courtieu | 2006-10-23 08:42:44 +0000 |
| commit | 01c61a9fdc76d4743a4ba23fd4b76acc5d6adef5 (patch) | |
| tree | 06d18794bb3fca72717d2c984dd132d2839eabfb | |
| parent | fe284842ffd97f02bc0954abadc201a7048512b1 (diff) | |
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
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 1 insertions, 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 |