Commit 36c5a842 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typo.

parent f24fd7c3
......@@ -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) :=
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment