1 files changed, 6 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