Standardize handling of Automatic Introduction.

This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.

2 files changed, 9 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5cead11a5c..1646906daa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1062,6 +1062,12 @@ let intros_replacing ids =
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
   end
 
+(* 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)
+
 (* User-level introduction tactics *)
 
 let lookup_hypothesis_as_renamed env sigma ccl = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7efadb2c28..b298524ff8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -70,6 +70,9 @@ val intros_using         : Id.t list -> unit Proofview.tactic
 val intros_replacing     : Id.t list -> unit Proofview.tactic
 val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
 
+(** [auto_intros_tac names] handles Automatic Introduction of binders *)
+val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
+
 val intros               : unit Proofview.tactic
 
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in