diff --git a/theories/tactics.v b/theories/tactics.v
index f9a13635ded1d863f8c9ce21ff5fe1ebbf82020a..55da19a4666ca6008dd24b59a9f078fed8433576 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -432,9 +432,9 @@ Ltac intros_revert tac :=
   | |- _ => tac
   end.
 
-(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
-runs [tac x] for each element [x] until [tac x] succeeds. If it does not
-suceed for any element of the generated list, the whole tactic wil fail. *)
+(** The tactic [iter tac l] runs [tac x] for each element [x ∈ l] until [tac x]
+succeeds. If it does not suceed for any element of the generated list, the whole
+tactic wil fail. *)
 Tactic Notation "iter" tactic(tac) tactic(l) :=
   let rec go l :=
   match l with ?x :: ?l => tac x || go l end in go l.