From b5f67e55e4bf901bc7bc85e6e93ab003a204ae4f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Apr 2020 15:46:16 +0200
Subject: [PATCH] Fix weird comment.

---
 theories/tactics.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index f9a13635..55da19a4 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.
-- 
GitLab