diff --git a/theories/tactics.v b/theories/tactics.v
index 4b884f34be8d386b67149a3d8f4d0022d0dae99a..807d1159c3c1499f2ea20d5100f6065591829171 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -357,7 +357,7 @@ Tactic Notation "iter" tactic(tac) tactic(l) :=
   let rec go l :=
   match l with ?x :: ?l => tac x || go l end in go l.
 
-(** Given H : [A_1 → ... → A_n → B] (where each [A_i] is non-dependent), the
+(** Given [H : A_1 → ... → A_n → B] (where each [A_i] is non-dependent), the
 tactic [feed tac H tac_by] creates a subgoal for each [A_i] and calls [tac p]
 with the generated proof [p] of [B]. *)
 Tactic Notation "feed" tactic(tac) constr(H) :=