diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 10:37:10 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 10:37:10 +0100 |
| commit | 563199757c5756fb5858da1b684162566a73fa3e (patch) | |
| tree | 0c320308919b973a82c1c6ca68edbf0e6c4054e4 /tactics | |
| parent | 7aaab2936e94eed9bc56eeb8430e0821158af86a (diff) | |
| parent | 5968648f9e9db09de462dd8c3530febd66466312 (diff) | |
Merge PR #6582: Mangle auto-generated names
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b41df7f75..20ada48a1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -388,12 +388,11 @@ let find_name mayrepl decl naming gl = match naming with new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> - (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let id' = next_ident_away id ids_of_hyps in - if not mayrepl && not (Id.equal id' id) then - user_err ?loc (Id.print id ++ str" is already used."); - id + (* When name is given, we allow to hide a global name *) + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in + if not mayrepl && Id.Set.mem id ids_of_hyps then + user_err ?loc (Id.print id ++ str" is already used."); + id (**************************************************************) (* Computing position of hypotheses for replacing *) |