From ed15664a6ab104c6184c5aae808169de6b64544f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Nov 2016 13:07:59 +0100
Subject: [PATCH] Fix typo.

---
 theories/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 4b884f34..807d1159 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) :=
-- 
GitLab