diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9e9d52b72c..5b1d7dabba 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1063,9 +1063,16 @@ let intros_replacing ids = (* The standard for implementing Automatic Introduction *) let auto_intros_tac ids = - Tacticals.New.tclMAP (function - | Name id -> intro_mustbe_force id - | Anonymous -> intro) (List.rev ids) + let fold used = function + | Name id -> Id.Set.add id used + | Anonymous -> used + in + let avoid = NamingAvoid (List.fold_left fold Id.Set.empty ids) in + let naming = function + | Name id -> NamingMustBe CAst.(make id) + | Anonymous -> avoid + in + Tacticals.New.tclMAP (fun name -> intro_gen (naming name) MoveLast true false) (List.rev ids) (* User-level introduction tactics *) |