diff options
| -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 433b64c32..2befb7e42 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 |